Commit 2021-01-18 07:03 db617b3c

View on Github →

feat(ring_theory/ideal/operations): add algebra structure on quotient (#5703) I added very basic stuff about R/I as an R-algebra that are missing in mathlib.

Estimated changes

Modified src/ring_theory/ideal/operations.lean

added def ideal.quotient.mkₐ

added theorem ideal.quotient.mkₐ_eq_mk

added theorem ideal.quotient.mkₐ_ker

added theorem ideal.quotient.mkₐ_surjective

added theorem ideal.quotient.mkₐ_to_ring_hom