Commit 2024-02-02 21:55 b1b4ebf7

View on Github →

chore(FiniteDimensional): rename lemmas (#10188) Rename lemmas to enable new-style dot notation or drop repeating FiniteDimensional.finiteDimensional_*. Restore old names as deprecated aliases.

Estimated changes

Modified Archive/Imo/Imo2019Q2.lean

Modified Mathlib/Analysis/InnerProductSpace/Orientation.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

deleted theorem FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two

added theorem FiniteDimensional.of_fact_finrank_eq_two

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

added theorem FiniteDimensional.of_isCompact_closedBall

added theorem FiniteDimensional.of_isCompact_closedBall₀

added theorem FiniteDimensional.of_locallyCompactSpace

deleted theorem finiteDimensional_of_isCompact_closedBall

deleted theorem finiteDimensional_of_isCompact_closedBall₀

deleted theorem finiteDimensional_of_locallyCompactSpace

Modified Mathlib/FieldTheory/KrullTopology.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

added theorem Field.FiniteDimensional.of_exists_primitive_element

added theorem Field.FiniteDimensional.of_finite_intermediateField

deleted theorem Field.finiteDimensional_of_exists_primitive_element

deleted theorem Field.finiteDimensional_of_finite_intermediateField

Modified Mathlib/FieldTheory/Tower.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional.lean

deleted theorem FiniteDimensional.fact_finiteDimensional_of_finrank_eq_succ

deleted theorem FiniteDimensional.finiteDimensional_of_finrank

deleted theorem FiniteDimensional.finiteDimensional_of_finrank_eq_succ

added theorem FiniteDimensional.of_fact_finrank_eq_succ

added theorem FiniteDimensional.of_finrank_eq_succ

added theorem FiniteDimensional.of_finrank_pos

added theorem FiniteDimensional.of_rank_eq_nat

added theorem FiniteDimensional.of_rank_eq_one

added theorem FiniteDimensional.of_rank_eq_zero

deleted theorem finiteDimensional_of_rank_eq_nat

deleted theorem finiteDimensional_of_rank_eq_one

deleted theorem finiteDimensional_of_rank_eq_zero

Modified Mathlib/LinearAlgebra/Orientation.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified docs/undergrad.yaml