Commit 2021-11-08 13:14 0dabcb8e

View on Github →

chore(ring_theory/ideal/operations): relax the base ring of algebras from comm_ring to comm_semiring (#10024) This also tidies up some variables and consistently uses B instead of S for the second algebra. One proof in ring_theory/finiteness.lean has to be redone because typeclass search times out where it previously did not. Thankfully, the new proof is shorter anyway.

Estimated changes

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/ideal/operations.lean

modified theorem ideal.algebra_map_quotient_injective

modified theorem ideal.ker_lift.map_smul

modified def ideal.ker_lift_alg

modified theorem ideal.ker_lift_alg_injective

modified theorem ideal.ker_lift_alg_mk

modified theorem ideal.ker_lift_alg_to_ring_hom

modified theorem ideal.quotient.mk_algebra_map

modified def ideal.quotient.mkₐ

modified theorem ideal.quotient.mkₐ_ker

modified theorem ideal.quotient.mkₐ_surjective

modified def ideal.quotient_equiv_alg

modified theorem ideal.quotient_ker_alg_equiv_of_right_inverse.apply

modified theorem ideal.quotient_ker_alg_equiv_of_right_inverse_symm.apply

modified theorem ideal.quotient_map_comp_mkₐ

modified theorem ideal.quotient_map_mkₐ

modified def ideal.quotient_mapₐ