mathlib

6fa678fb - feat(ring_theory): `coe_submodule S (⊤ : ideal R) = 1` (#8272)

feat(ring_theory): `coe_submodule S (⊤ : ideal R) = 1` (#8272) A little `simp` lemma and its dependencies. As I was implementing it, I saw the definition of `has_one (submodule R A)` can be cleaned up a bit.