Commit 2025-12-31 06:46 52e2525f

View on Github →

chore(RingTheory/FiniteType): move MonoidAlgebra lemmas earlier (#33099) ... and deduce them from a missing Finsupp lemma

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

modified theorem AddMonoidAlgebra.liftNC_smul

added theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure

added theorem AddMonoidAlgebra.of'_mem_span

modified theorem MonoidAlgebra.liftNC_smul

added theorem MonoidAlgebra.mem_closure_of_mem_span_closure

added theorem MonoidAlgebra.of_mem_span_of_iff

modified theorem MonoidAlgebra.smul_of

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

added theorem Finsupp.single_mem_span_single

Modified Mathlib/RingTheory/FiniteType.lean

deleted theorem AddMonoidAlgebra.mem_closure_of_mem_span_closure

deleted theorem AddMonoidAlgebra.of'_mem_span

deleted theorem MonoidAlgebra.mem_closure_of_mem_span_closure

deleted theorem MonoidAlgebra.of_mem_span_of_iff