mathlib3

49ab444f - fix(algebra/module/submodule_lattice): correct bad lemma (#9809)

fix(algebra/module/submodule_lattice): correct bad lemma (#9809) This lemma was accidentally stating that inf and inter are the same on sets, and wasn't about submodule at all. The old statement was `↑p ⊓ ↑q = ↑p ∩ ↑q`, the new one is `↑(p ⊓ q) = ↑p ∩ ↑q`