Theorem Submodule.one_eq_range

Modification history

2024-10-26 13:22

Mathlib/Algebra/Algebra/Operations.lean

refactor: change the definition of `1 : Submodule R A` to the range of `(· • 1)` (#18092) …

Modified Submodule.one_eq_range View on Github →

2023-03-04 17:16

Mathlib/Algebra/Algebra/Operations.lean

feat: port Algebra.Algebra.Operations (#2568) …

Added Submodule.one_eq_range View on Github →