Theorem NonUnitalSubalgebra.coe_toNonUnitalSubring

Modification history

2023-11-04 00:57

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

chore(Algebra/Algebra/NonUnitalSubalgebra): generalize lemmas to non-associative cases (#8147) …

Modified NonUnitalSubalgebra.coe_toNonUnitalSubring View on Github →

2023-07-03 00:43

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

feat: define `NonUnitalSubalgebra` and develop basic API (#5512) …

Added NonUnitalSubalgebra.coe_toNonUnitalSubring View on Github →