Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 309da201

View on Github →

feat(*): Random lemmas about adjoin/span. (#10666)

Estimated changes

Modified src/algebra/pointwise.lean

added theorem submonoid.pow_smul_mem_closure_smul

Modified src/group_theory/submonoid/membership.lean

added theorem submonoid.map_powers

Modified src/linear_algebra/basic.lean

added theorem submodule.span_attach_bUnion

added theorem submodule.span_smul_eq_of_is_unit

added theorem submodule.span_smul_le

Modified src/ring_theory/adjoin/basic.lean

added theorem algebra.adjoin_Union

added theorem algebra.adjoin_attach_bUnion

added theorem algebra.adjoin_eq_Inf

added theorem algebra.pow_smul_mem_adjoin_smul

Modified src/ring_theory/ideal/operations.lean

added theorem submodule.ideal_span_singleton_smul

added theorem submodule.mem_of_span_top_of_smul_mem

added theorem submodule.span_smul_eq

added theorem submodule.union_eq_smul_set