Commit 2021-07-12 16:03 6fa678fb
View on Github →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.