Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-19 03:33 04fe4b6d

View on Github →

feat(algebra/ring_quot): quotients of noncommutative rings (#4078)

Estimated changes

Created src/algebra/ring_quot.lean

added theorem ring_quot.eq_lift_alg_hom_comp_mk_alg_hom

added theorem ring_quot.eq_lift_comp_mk_ring_hom

added def ring_quot.ideal_quotient_to_ring_quot

added theorem ring_quot.ideal_quotient_to_ring_quot_apply

added def ring_quot.lift

added def ring_quot.lift_alg_hom

added theorem ring_quot.lift_alg_hom_mk_alg_hom_apply

added theorem ring_quot.lift_alg_hom_unique

added theorem ring_quot.lift_mk_ring_hom_apply

added theorem ring_quot.lift_unique

added def ring_quot.mk_alg_hom

added theorem ring_quot.mk_alg_hom_coe

added theorem ring_quot.mk_alg_hom_rel

added theorem ring_quot.mk_alg_hom_surjective

added def ring_quot.mk_ring_hom

added theorem ring_quot.mk_ring_hom_rel

added theorem ring_quot.mk_ring_hom_surjective

added theorem ring_quot.rel.add_right

added theorem ring_quot.rel.neg

added theorem ring_quot.rel.smul

added inductive ring_quot.rel

added def ring_quot.ring_quot_equiv_ideal_quotient

added theorem ring_quot.ring_quot_ext'

added theorem ring_quot.ring_quot_ext

added def ring_quot.ring_quot_to_ideal_quotient

added theorem ring_quot.ring_quot_to_ideal_quotient_apply

added def ring_quot

Modified src/data/equiv/ring.lean

added def ring_equiv.of_hom_inv

added theorem ring_equiv.of_hom_inv_apply

added theorem ring_equiv.of_hom_inv_symm_apply

Modified src/linear_algebra/basic.lean

added theorem submodule.mem_Inf

Modified src/ring_theory/ideal/basic.lean

added def ideal.of_rel