Commit 2024-01-09 00:24 a131be44

View on Github →

feat: z⁻¹ = conj z when z has norm one (#9535) and other simple lemmas From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.conj_mul'

added theorem Complex.exists_norm_eq_mul_self

added theorem Complex.exists_norm_mul_eq_self

added theorem Complex.inv_eq_conj

added theorem Complex.mul_conj'

added theorem Complex.norm_I

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/NormedSpace/Extend.lean

Modified Mathlib/Data/IsROrC/Basic.lean

added theorem IsROrC.conj_div

modified theorem IsROrC.conj_mul

added theorem IsROrC.exists_norm_eq_mul_self

added theorem IsROrC.exists_norm_mul_eq_self

added theorem IsROrC.inv_eq_conj

modified theorem IsROrC.lt_iff_re_im

modified theorem IsROrC.mul_conj

modified theorem IsROrC.neg_iff

added theorem IsROrC.neg_iff_exists_ofReal

modified theorem IsROrC.nonneg_iff

added theorem IsROrC.nonneg_iff_exists_ofReal

modified theorem IsROrC.nonpos_iff

added theorem IsROrC.nonpos_iff_exists_ofReal

modified theorem IsROrC.pos_iff

added theorem IsROrC.pos_iff_exists_ofReal

Modified Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean