Commit 2025-05-19 06:33 b78122b3

View on Github →

feat: miscellaneous lemmas about transcendence bases (#24344)

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

modified theorem NeZero.of_faithfulSMul

deleted theorem faithfulSMul_iff_injective_smul_one

Modified Mathlib/Algebra/Group/Action/Faithful.lean

added theorem faithfulSMul_iff_injective_smul_one

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

added theorem IntermediateField.finite_of_fg_of_isAlgebraic

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

added theorem IntermediateField.finrank_eq_one_iff_eq_top

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

added theorem isSeparable_iff_finInsepDegree_eq_one

Modified Mathlib/FieldTheory/Separable.lean

added theorem IsSeparable.map

Modified Mathlib/FieldTheory/SeparableClosure.lean

added theorem Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower

added theorem Field.insepDegree_le_of_left_le

added theorem Field.insepDegree_le_rank

added theorem Field.insepDegree_top_le_insepDegree_of_isScalarTower

added theorem Field.sepDegree_le_rank

added theorem IntermediateField.finInsepDegree_le_of_left_le

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem Module.lift_rank_bot_le_lift_rank_of_isScalarTower

added theorem Module.rank_bot_le_rank_of_isScalarTower

added theorem Module.rank_top_le_rank_of_isScalarTower

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem Module.finrank_bot_le_finrank_of_isScalarTower_of_free

added theorem Module.finrank_top_le_finrank_of_isScalarTower_of_free

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

added theorem Module.finrank_bot_le_finrank_of_isScalarTower

added theorem Module.finrank_top_le_finrank_of_isScalarTower

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

added theorem LinearIndependent.restrict_scalars'

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

deleted theorem LinearIndependent.restrict_scalars'

Modified Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

added theorem IsTranscendenceBasis.of_comp

added theorem IsTranscendenceBasis.of_comp_algebraMap

Modified Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

added theorem IsTranscendenceBasis.algebraMap_comp

added theorem IsTranscendenceBasis.isAlgebraic_iff

Modified Mathlib/RingTheory/Norm/Basic.lean