Commit 2024-12-03 07:56 5358a537

View on Github →

chore(Data/Int): move Pi.instIntCast (#19612) This instance was found in Data.Int.Cast.Lemmas and is used quite a few times without all the theory in those files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

deleted theorem Pi.intCast_apply

deleted theorem Pi.intCast_def

deleted theorem Sum.elim_intCast_intCast

Created Mathlib/Data/Int/Cast/Pi.lean

added theorem Pi.intCast_apply

added theorem Pi.intCast_def

added theorem Sum.elim_intCast_intCast

Modified Mathlib/Data/Int/CharZero.lean

Modified Mathlib/Data/Matrix/Diagonal.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean