Commit 2023-11-04 00:57 035f4246

View on Github →

chore(Algebra/Algebra/NonUnitalSubalgebra): generalize lemmas to non-associative cases (#8147) Notably this generalizes instNonUnitalSubringClass and makes toNonUnitalSubring work in the non-associative case. The types themselves were already sufficiently general.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

modified theorem NonUnitalAlgebra.top_toSubring

modified theorem NonUnitalSubalgebra.coe_toNonUnitalSubring

modified theorem NonUnitalSubalgebra.mem_toNonUnitalSubring

modified def NonUnitalSubalgebra.toNonUnitalSubring'

modified def NonUnitalSubalgebra.toNonUnitalSubring

modified theorem NonUnitalSubalgebra.toNonUnitalSubring_inj

modified theorem NonUnitalSubalgebra.toNonUnitalSubring_injective

modified def NonUnitalSubalgebra.toNonUnitalSubsemiring'

modified def NonUnitalSubalgebra.toSubmodule'