Commit 2023-12-18 10:05 8eef7faf

View on Github →

feat: demote the instance Fintype.ofIsEmpty to a def (#8816) Rationale: this instance creates (empty) data out of nothing, which may conflict with other data. If you have in the context [Fintype i] and case on whether i is empty or not, then this gave two non-defeq instances of [Fintype i] around.

Estimated changes

Modified Archive/ZagierTwoSquares.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Data/Fintype/Basic.lean

added def Fintype.ofIsEmpty

modified theorem Fintype.univ_of_isEmpty

Modified Mathlib/Data/Fintype/Card.lean

modified theorem Fintype.card_eq_zero

modified theorem Fintype.card_of_isEmpty

Modified Mathlib/Data/Fintype/CardEmbedding.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/LinearAlgebra/Orientation.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

modified theorem MeasureTheory.Measure.pi_empty_univ

modified theorem MeasureTheory.Measure.pi_of_empty

modified theorem MeasureTheory.measurePreserving_pi_empty

modified theorem MeasureTheory.volume_preserving_pi_empty

Modified Mathlib/ModelTheory/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

deleted theorem Nat.card_eq_zero_of_isEmpty

modified theorem Nat.card_of_isEmpty

Modified Mathlib/SetTheory/Game/Short.lean

modified def SetTheory.PGame.Short.ofIsEmpty