Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-23 09:46 3ff92489

View on Github →

feat({group,ring}theory/free*): make free_ring.lift and free_comm_ring.lift equivs (#6364) This also adds free_ring.hom_ext and free_comm_ring.hom_ext, and deduplicates the definitions of the two lifts by introducing abelian_group.lift_monoid.

Estimated changes

Modified src/algebra/direct_limit.lean

Modified src/group_theory/free_abelian_group.lean

added def free_abelian_group.lift_monoid

added theorem free_abelian_group.lift_monoid_coe

added theorem free_abelian_group.lift_monoid_coe_add_monoid_hom

added theorem free_abelian_group.lift_monoid_symm_coe

modified theorem free_abelian_group.mul_def

modified theorem free_abelian_group.of_mul

added def free_abelian_group.of_mul_hom

added theorem free_abelian_group.of_mul_hom_coe

modified theorem free_abelian_group.of_mul_of

modified theorem free_abelian_group.of_one

modified theorem free_abelian_group.one_def

Modified src/ring_theory/free_comm_ring.lean

added theorem free_comm_ring.hom_ext

modified def free_comm_ring.lift

Modified src/ring_theory/free_ring.lean

added theorem free_ring.hom_ext

modified def free_ring.lift