feat(ring_theory/adjoin/basic): lemmas relating adjoin and submodule.span (#8031)
feat(ring_theory/adjoin/basic): lemmas relating adjoin and submodule.span (#8031)







leanprover-community/mathlib,leanprover-community/mathlib