Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-19 08:28 3ba7d128

View on Github →

feat(algebra): obtaining algebraic classes through in/surjective maps (#2638) This is needed for the definition of Witt vectors.

Estimated changes

Created src/algebra/inj_surj.lean

added def comm_group_of_injective

added def comm_group_of_surjective

added def comm_monoid_of_injective

added def comm_monoid_of_surjective

added def comm_ring_of_injective

added def comm_ring_of_surjective

added def comm_semigroup_of_injective

added def comm_semigroup_of_surjective

added def comm_semiring_of_injective

added def comm_semiring_of_surjective

added def group_of_injective

added def group_of_surjective

added def monoid_of_injective

added def monoid_of_surjective

added def ring_of_injective

added def ring_of_surjective

added def semigroup_of_injective

added def semigroup_of_surjective

added def semiring_of_injective

added def semiring_of_surjective