Commit 2024-07-15 10:14 ad047c62

View on Github →

chore: split LinearAlgebra.FiniteDimensional (#14670) This splits out everything that only depends on FieldTheory.Finiteness.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean

Modified Mathlib/Data/Complex/FiniteDimensional.lean

Modified Mathlib/Data/Matrix/Rank.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/FieldTheory/Tower.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

deleted theorem FiniteDimensional.basisSingleton_apply

deleted theorem FiniteDimensional.eq_of_le_of_finrank_eq

deleted theorem FiniteDimensional.eq_of_le_of_finrank_le

deleted theorem FiniteDimensional.exists_mul_eq_one

deleted theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card

deleted theorem FiniteDimensional.finiteDimensional_iff_of_rank_eq_nsmul

deleted theorem FiniteDimensional.finite_of_finite

deleted theorem FiniteDimensional.finrank_eq_card_basis'

deleted theorem FiniteDimensional.finrank_eq_rank'

deleted theorem FiniteDimensional.finrank_of_infinite_dimensional

deleted theorem FiniteDimensional.of_fact_finrank_eq_succ

deleted theorem FiniteDimensional.of_finite_basis

deleted theorem FiniteDimensional.of_finrank_eq_succ

deleted theorem FiniteDimensional.of_finrank_pos

deleted theorem FiniteDimensional.of_fintype_basis

deleted theorem FiniteDimensional.of_injective

deleted theorem FiniteDimensional.of_rank_eq_nat

deleted theorem FiniteDimensional.of_rank_eq_one

deleted theorem FiniteDimensional.of_rank_eq_zero

deleted theorem FiniteDimensional.of_surjective

deleted theorem FiniteDimensional.range_basisSingleton

deleted theorem FiniteDimensional.span_of_finite

deleted theorem FiniteDimensional.trans

deleted theorem LinearEquiv.coe_ofInjectiveEndo

deleted theorem LinearEquiv.ofInjectiveEndo_left_inv

deleted theorem LinearEquiv.ofInjectiveEndo_right_inv

deleted theorem LinearIndependent.lt_aleph0_of_finiteDimensional

deleted theorem LinearMap.comap_eq_sup_ker_of_disjoint

deleted theorem LinearMap.comp_eq_id_comm

deleted theorem LinearMap.finiteDimensional_of_surjective

deleted theorem LinearMap.injOn_iff_surjOn

deleted theorem LinearMap.injective_iff_surjective

deleted theorem LinearMap.isUnit_iff_ker_eq_bot

deleted theorem LinearMap.isUnit_iff_range_eq_top

deleted theorem LinearMap.ker_comp_eq_of_commute_of_disjoint_ker

deleted theorem LinearMap.ker_eq_bot_iff_range_eq_top

deleted theorem LinearMap.ker_noncommProd_eq_of_supIndep_ker

deleted theorem LinearMap.mul_eq_one_comm

deleted theorem LinearMap.mul_eq_one_of_mul_eq_one

deleted theorem LinearMap.surjective_of_injective

deleted theorem Module.End.ker_pow_constant

deleted theorem Set.finrank_mono

deleted theorem Subalgebra.eq_of_le_of_finrank_eq

deleted theorem Subalgebra.eq_of_le_of_finrank_le

deleted theorem Subalgebra.finiteDimensional_bot

deleted theorem Subalgebra.finiteDimensional_toSubmodule

deleted theorem Submodule.eq_top_of_finrank_eq

deleted theorem Submodule.fg_iff_finiteDimensional

deleted theorem Submodule.finiteDimensional_of_le

deleted theorem Submodule.finrank_mono

deleted theorem exists_smul_eq_of_finrank_eq_one

deleted theorem finrank_eq_one_iff_of_nonzero'

deleted theorem finrank_eq_one_iff_of_nonzero

deleted theorem finrank_span_singleton

deleted theorem finrank_zero_iff_forall_zero

deleted theorem surjective_of_nonzero_of_finrank_eq_one

Created Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

added theorem FiniteDimensional.basisSingleton_apply

added theorem FiniteDimensional.eq_of_le_of_finrank_eq

added theorem FiniteDimensional.eq_of_le_of_finrank_le

added theorem FiniteDimensional.exists_mul_eq_one

added theorem FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card

added theorem FiniteDimensional.finiteDimensional_iff_of_rank_eq_nsmul

added theorem FiniteDimensional.finite_of_finite

added theorem FiniteDimensional.finrank_eq_card_basis'

added theorem FiniteDimensional.finrank_eq_rank'

added theorem FiniteDimensional.finrank_of_infinite_dimensional

added theorem FiniteDimensional.of_fact_finrank_eq_succ

added theorem FiniteDimensional.of_finite_basis

added theorem FiniteDimensional.of_finrank_eq_succ

added theorem FiniteDimensional.of_finrank_pos

added theorem FiniteDimensional.of_fintype_basis

added theorem FiniteDimensional.of_injective

added theorem FiniteDimensional.of_rank_eq_nat

added theorem FiniteDimensional.of_rank_eq_one

added theorem FiniteDimensional.of_rank_eq_zero

added theorem FiniteDimensional.of_surjective

added theorem FiniteDimensional.range_basisSingleton

added theorem FiniteDimensional.span_of_finite

added theorem FiniteDimensional.trans

added theorem LinearEquiv.coe_ofInjectiveEndo

added theorem LinearEquiv.ofInjectiveEndo_left_inv

added theorem LinearEquiv.ofInjectiveEndo_right_inv

added theorem LinearIndependent.lt_aleph0_of_finiteDimensional

added theorem LinearMap.comap_eq_sup_ker_of_disjoint

added theorem LinearMap.comp_eq_id_comm

added theorem LinearMap.finiteDimensional_of_surjective

added theorem LinearMap.injOn_iff_surjOn

added theorem LinearMap.injective_iff_surjective

added theorem LinearMap.isUnit_iff_ker_eq_bot

added theorem LinearMap.isUnit_iff_range_eq_top

added theorem LinearMap.ker_comp_eq_of_commute_of_disjoint_ker

added theorem LinearMap.ker_eq_bot_iff_range_eq_top

added theorem LinearMap.ker_noncommProd_eq_of_supIndep_ker

added theorem LinearMap.mul_eq_one_comm

added theorem LinearMap.mul_eq_one_of_mul_eq_one

added theorem LinearMap.surjective_of_injective

added theorem Module.End.ker_pow_constant

added theorem Set.finrank_mono

added theorem Subalgebra.eq_of_le_of_finrank_eq

added theorem Subalgebra.eq_of_le_of_finrank_le

added theorem Subalgebra.finiteDimensional_bot

added theorem Subalgebra.finiteDimensional_toSubmodule

added theorem Submodule.eq_top_of_finrank_eq

added theorem Submodule.fg_iff_finiteDimensional

added theorem Submodule.finiteDimensional_of_le

added theorem Submodule.finrank_mono

added theorem exists_smul_eq_of_finrank_eq_one

added theorem finrank_eq_one_iff_of_nonzero'

added theorem finrank_eq_one_iff_of_nonzero

added theorem finrank_span_singleton

added theorem finrank_zero_iff_forall_zero

added theorem surjective_of_nonzero_of_finrank_eq_one

Modified Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

Modified Mathlib/LinearAlgebra/Projectivization/Basic.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified Mathlib/RingTheory/Algebraic.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/RingTheory/IntegralClosure.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Norm/Defs.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

Modified Mathlib/Topology/Instances/Complex.lean