Commit 2023-09-12 04:12 260cb506

View on Github →

refactor: split Algebra.Hom.Group and Algebra.Hom.Ring (#7094)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

Modified Mathlib/Algebra/Divisibility/Basic.lean

Modified Mathlib/Algebra/Field/Basic.lean

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Algebra/Group/Conj.lean

Modified Mathlib/Algebra/Group/Ext.lean

Modified Mathlib/Algebra/Group/Pi.lean

Modified Mathlib/Algebra/Group/TypeTags.lean

Modified Mathlib/Algebra/GroupPower/Ring.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

Modified Mathlib/Algebra/Hom/Commute.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

Created Mathlib/Algebra/Hom/Group/Basic.lean

added theorem MonoidHom.coe_of_map_div

added theorem MonoidHom.coe_of_map_mul_inv

added theorem MonoidHom.comp_inv

added theorem MonoidHom.comp_mul

added theorem MonoidHom.div_apply

added theorem MonoidHom.inv_apply

added theorem MonoidHom.inv_comp

added theorem MonoidHom.mul_apply

added theorem MonoidHom.mul_comp

added def MonoidHom.ofMapDiv

added def MonoidHom.ofMapMulInv

added theorem MulHom.comp_mul

added theorem MulHom.mul_apply

added theorem MulHom.mul_comp

added theorem NeZero.of_injective

added theorem NeZero.of_map

added theorem coe_invMonoidHom

added theorem injective_iff_map_eq_one'

added theorem injective_iff_map_eq_one

added def invMonoidHom

added theorem invMonoidHom_apply

Renamed Mathlib/Algebra/Hom/Group.lean to Mathlib/Algebra/Hom/Group/Defs.lean

deleted theorem MonoidHom.coe_of_map_div

deleted theorem MonoidHom.coe_of_map_mul_inv

deleted theorem MonoidHom.comp_inv

deleted theorem MonoidHom.comp_mul

deleted theorem MonoidHom.div_apply

deleted theorem MonoidHom.inv_apply

deleted theorem MonoidHom.inv_comp

deleted theorem MonoidHom.mul_apply

deleted theorem MonoidHom.mul_comp

deleted def MonoidHom.ofMapDiv

deleted def MonoidHom.ofMapMulInv

deleted theorem MulHom.comp_mul

deleted theorem MulHom.mul_apply

deleted theorem MulHom.mul_comp

deleted theorem NeZero.of_injective

deleted theorem NeZero.of_map

deleted theorem coe_invMonoidHom

deleted theorem injective_iff_map_eq_one'

deleted theorem injective_iff_map_eq_one

deleted def invMonoidHom

deleted theorem invMonoidHom_apply

Modified Mathlib/Algebra/Hom/GroupInstances.lean

Created Mathlib/Algebra/Hom/Ring/Basic.lean

added theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero

added theorem RingHom.isUnit_map

Renamed Mathlib/Algebra/Hom/Ring.lean to Mathlib/Algebra/Hom/Ring/Defs.lean

deleted theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero

deleted theorem RingHom.isUnit_map

Modified Mathlib/Algebra/Hom/Units.lean

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Ring/Opposite.lean

Modified Mathlib/Algebra/Ring/Pi.lean

Modified Mathlib/CategoryTheory/Groupoid/VertexGroup.lean

Modified Mathlib/CategoryTheory/Monoidal/Discrete.lean

Modified Mathlib/CategoryTheory/Preadditive/Basic.lean

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

Modified Mathlib/Data/List/BigOperators/Lemmas.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Deprecated/Group.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/Submonoid/Basic.lean

Modified Mathlib/GroupTheory/Subsemigroup/Basic.lean

Modified Mathlib/RingTheory/Congruence.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

Modified test/symm.lean