Commit 2021-10-20 11:46 49ab444f
View on Github →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