Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-29 04:58 0bb5e5d9

View on Github →

feat(ring_theory/algebra_tower): Artin--Tate lemma (#4282)

Estimated changes

Modified src/field_theory/intermediate_field.lean

Modified src/linear_algebra/basic.lean

added theorem submodule.map_span

Modified src/linear_algebra/finsupp.lean

added theorem mem_span_finset

Modified src/ring_theory/adjoin.lean

added theorem algebra.adjoin_image

added theorem subalgebra.fg_adjoin_finset

added theorem subalgebra.fg_map

added theorem subalgebra.fg_of_fg_map

added theorem subalgebra.fg_of_submodule_fg

added theorem subalgebra.fg_top

Modified src/ring_theory/algebra.lean

added theorem subalgebra.coe_val

added theorem subalgebra.map_injective

added theorem subalgebra.map_mono

added theorem subalgebra.range_val

Modified src/ring_theory/algebra_tower.lean

added theorem algebra.fg_trans'

added theorem exists_subalgebra_of_fg

added theorem fg_of_fg_of_fg

modified theorem is_scalar_tower.aeval_apply

modified theorem is_scalar_tower.of_algebra_map_eq

Modified src/ring_theory/noetherian.lean

added theorem fg_of_injective

added theorem is_noetherian_of_fg_of_noetherian'

added theorem is_noetherian_of_injective

added theorem submodule.fg_of_fg_map

modified theorem submodule.fg_of_fg_map_of_fg_inf_ker

added theorem submodule.fg_of_linear_equiv

added theorem submodule.fg_top