Theorem NonUnitalSubalgebra.toNonUnitalSubring_injective

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.toNonUnitalSubring_injective View on Github →

2023-07-03 00:43

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

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

Added NonUnitalSubalgebra.toNonUnitalSubring_injective View on Github →