Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 12:18 42bb0c4b

View on Github →

feat(ring_theory/ideal/operations): add first isomorphism theorem for rings and algebras (#6166) The first isomorphism theorem for commutative rings quotient_ker_equiv_of_surjective and algebras quotient_ker_alg_equiv_of_surjective.

Estimated changes

Modified docs/overview.yaml

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.ker_lift.map_smul

added def ideal.ker_lift_alg

added theorem ideal.ker_lift_alg_injective

added theorem ideal.ker_lift_alg_mk

added theorem ideal.ker_lift_alg_to_ring_hom

added theorem ideal.quotient_ker_alg_equiv_of_right_inverse.apply

added def ideal.quotient_ker_alg_equiv_of_right_inverse

added theorem ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply

added def ring_hom.ker_lift

added theorem ring_hom.ker_lift_injective

added theorem ring_hom.ker_lift_mk

added theorem ring_hom.quotient_ker_equiv_of_right_inverse.apply

added theorem ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply

added def ring_hom.quotient_ker_equiv_of_right_inverse