Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 05:06 792f5415

View on Github →

feat(field_theory/tower): tower law (#3355)

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_extend_by_one

Modified src/algebra/pointwise.lean

added theorem set.range_smul_range

Modified src/data/finset/basic.lean

added theorem finset.subset_product

Created src/field_theory/tower.lean

added theorem dim_mul_dim'

added theorem dim_mul_dim

added theorem finite_dimensional.findim_mul_findim

added theorem finite_dimensional.trans

Modified src/linear_algebra/basis.lean

added theorem linear_independent_iff''

Modified src/ring_theory/algebra_tower.lean

modified theorem is_algebra_tower.algebra_map_apply

modified theorem is_algebra_tower.algebra_map_eq

added theorem is_algebra_tower.algebra_map_smul

added theorem is_algebra_tower.smul_left_comm

added theorem is_basis.smul

added theorem linear_independent_smul

added def submodule.restrict_scalars'

added theorem submodule.restrict_scalars'_inj

added theorem submodule.restrict_scalars'_injective

added theorem submodule.restrict_scalars'_top

added theorem submodule.smul_mem_span_smul'

added theorem submodule.smul_mem_span_smul

added theorem submodule.smul_mem_span_smul_of_mem

added theorem submodule.span_smul