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