pith. machine review for the scientific record. sign in
theorem proved term proof

eq_iff_toComplex_eq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  66theorem eq_iff_toComplex_eq {z w : LogicComplex} :
  67    z = w ↔ toComplex z = toComplex w := by

proof body

Term-mode proof.

  68  constructor
  69  · exact congrArg toComplex
  70  · intro h
  71    have := congrArg fromComplex h
  72    rw [fromComplex_toComplex, fromComplex_toComplex] at this
  73    exact this
  74
  75/-! ## Algebra and coordinate transport -/
  76
  77instance : Zero LogicComplex := ⟨fromComplex 0⟩
  78instance : One LogicComplex := ⟨fromComplex 1⟩
  79instance : Add LogicComplex := ⟨fun z w => fromComplex (toComplex z + toComplex w)⟩
  80instance : Neg LogicComplex := ⟨fun z => fromComplex (-toComplex z)⟩
  81instance : Sub LogicComplex := ⟨fun z w => fromComplex (toComplex z - toComplex w)⟩
  82instance : Mul LogicComplex := ⟨fun z w => fromComplex (toComplex z * toComplex w)⟩
  83instance : Inv LogicComplex := ⟨fun z => fromComplex (toComplex z)⁻¹⟩
  84instance : Div LogicComplex := ⟨fun z w => fromComplex (toComplex z / toComplex w)⟩
  85

depends on (5)

Lean names referenced from this declaration's body.