Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.one_eq_range

Modification history

2021-07-12 16:03
src/algebra/algebra/operations.lean
feat(ring_theory): `coe_submodule S (⊤ : ideal R) = 1` (#8272) …
Added submodule.one_eq_rangeView on Github →