mathlib

f45dee43 - feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641)

feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641) Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com> Co-authored-by: Ashvni <ashvni.n@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>