Commit 2023-09-15 17:12 fb84a08f

View on Github →

feat : Abelian groups has enough injectives (#7157)

Estimated changes

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

added theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.divBy_addOrderOf_addOrderOf

added theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_eq

added theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_eq_aux

added theorem AddCommGroupCat.enough_injectives_aux_proofs.finite_order.toRatCircle_apply_self_ne_zero

added theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_eq

added theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_eq_aux

added theorem AddCommGroupCat.enough_injectives_aux_proofs.infinite_order.toRatCircle_apply_self_ne_zero

added def AddCommGroupCat.enough_injectives_aux_proofs.next

added def AddCommGroupCat.enough_injectives_aux_proofs.presentation

added def AddCommGroupCat.enough_injectives_aux_proofs.toNext

added theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_inj

added theorem AddCommGroupCat.enough_injectives_aux_proofs.toNext_inj_of_exists

added theorem LinearMap.toSpanSingleton_ker

Modified Mathlib/GroupTheory/Divisible.lean