Commit 2023-09-19 07:20 6d8747c6

View on Github →

chore(GroupCat/Injective): golf (#7204)

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Injective.lean

added theorem AddCommGroupCat.enough_injectives_aux_proofs.divBy_self

added theorem AddCommGroupCat.enough_injectives_aux_proofs.eq_zero_of_toRatCircle_apply_self

added theorem AddCommGroupCat.enough_injectives_aux_proofs.equivZModSpanAddOrderOf_apply_self

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.divBy_addOrderOf_addOrderOf

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_eq

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_eq_aux

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_ne_zero

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_eq

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_eq_aux

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_ne_zero

modified def AddCommGroupCat.enough_injectives_aux_proofs.presentation

modified theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_inj

deleted theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_inj_of_exists

added theorem AddCommGroupCat.injective_as_module_iff

deleted theorem AddCommGroupCat.injective_as_module_of_injective_as_Ab

deleted theorem AddCommGroupCat.injective_of_injective_as_module

Modified Mathlib/CategoryTheory/Preadditive/Injective.lean

added theorem CategoryTheory.Equivalence.map_injective_iff

Modified Mathlib/CategoryTheory/Preadditive/Projective.lean

added theorem CategoryTheory.Equivalence.map_projective_iff