bookshelf/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean

19 lines
347 B
Plaintext
Raw Normal View History

/-
2023-04-02 14:57:58 +00:00
Chapter 1
2023-04-02 14:57:58 +00:00
Introduction and Examples
-/
import Mathlib.Data.Complex.Basic
open Complex
open HPow
-- In Exercises 1 through 9 compute the given arithmetic expression and give the
-- answer in the form $a + bi$ for $a, b ∈ $.
theorem ex1_1 : I^3 = 0 + (-1) * I := calc
I^3
= I * (I * hPow I 1) := rfl
2023-04-02 14:57:58 +00:00
_ = 0 + (-1) * I := by simp