Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-12-04 20:02
c982179e
View on Github →
feat(
/sub
/pointwise): lemmas about pointwise scalar actions (
#17814
)
Estimated changes
Modified
src/algebra/algebra/tower.lean
deleted
theorem
submodule.span_smul
added
theorem
submodule.span_smul_of_span_eq_top
Modified
src/algebra/module/submodule/pointwise.lean
added
theorem
submodule.smul_bot'
added
theorem
submodule.smul_span
added
theorem
submodule.smul_sup'
added
theorem
submodule.span_smul
Modified
src/group_theory/subgroup/pointwise.lean
modified
theorem
subgroup.smul_bot
added
theorem
subgroup.smul_closure
added
theorem
subgroup.smul_sup
Modified
src/group_theory/submonoid/pointwise.lean
added
theorem
add_submonoid.smul_bot
added
theorem
add_submonoid.smul_closure
added
theorem
add_submonoid.smul_sup
added
theorem
submonoid.smul_bot
added
theorem
submonoid.smul_closure
added
theorem
submonoid.smul_sup
Modified
src/ring_theory/finiteness.lean
Modified
src/ring_theory/ideal/operations.lean
deleted
theorem
submodule.span_smul_eq
Modified
src/ring_theory/local_properties.lean
Modified
src/ring_theory/subring/pointwise.lean
added
theorem
subring.smul_bot
added
theorem
subring.smul_closure
added
theorem
subring.smul_sup
Modified
src/ring_theory/subsemiring/pointwise.lean
added
theorem
subsemiring.smul_bot
added
theorem
subsemiring.smul_closure
added
theorem
subsemiring.smul_sup