Commit 2023-03-21 18:08 f02ff00e

View on Github →

chore: tidy various files (#2999)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Hom.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

added theorem CategoryTheory.Limits.inr_coprodZeroIso_hom

deleted theorem CategoryTheory.Limits.inr_coprod_zeroiso_hom

Modified Mathlib/Data/Complex/Basic.lean

deleted theorem Complex.ComplexOrder.eq_re_ofReal_le

deleted theorem Complex.ComplexOrder.le_def

deleted theorem Complex.ComplexOrder.lt_def

deleted theorem Complex.ComplexOrder.not_le_iff

deleted theorem Complex.ComplexOrder.not_le_zero_iff

deleted theorem Complex.ComplexOrder.not_lt_iff

deleted theorem Complex.ComplexOrder.not_lt_zero_iff

deleted theorem Complex.ComplexOrder.real_le_real

deleted theorem Complex.ComplexOrder.real_lt_real

deleted theorem Complex.ComplexOrder.zero_le_real

deleted theorem Complex.ComplexOrder.zero_lt_real

added theorem Complex.eq_re_ofReal_le

added theorem Complex.le_def

added theorem Complex.lt_def

added theorem Complex.not_le_iff

added theorem Complex.not_le_zero_iff

added theorem Complex.not_lt_iff

added theorem Complex.not_lt_zero_iff

modified theorem Complex.ofReal_rat_cast

modified theorem Complex.rat_cast_im

modified theorem Complex.rat_cast_re

added theorem Complex.real_le_real

added theorem Complex.real_lt_real

added theorem Complex.zero_le_real

added theorem Complex.zero_lt_real

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean