Commit 2026-10-29 15:19 c1ec7f6c

View on Github →

chore: protect Pi.*_apply lemmas (#45435) Prevent namespace conflicts in #45329.

Estimated changes

Modified Archive/Imo/Imo2010Q5.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Pi.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Group/Pi/Lemmas.lean

Modified Mathlib/Algebra/Group/TypeTags/Basic.lean

Modified Mathlib/Algebra/Notation/Pi/Basic.lean

Modified Mathlib/Algebra/Notation/Pi/Defs.lean

deleted theorem Pi.div_apply

deleted theorem Pi.inv_apply

deleted theorem Pi.mul_apply

deleted theorem Pi.one_apply

deleted theorem Pi.pow_apply

Modified Mathlib/Algebra/Order/Star/Pi.lean

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

deleted theorem Pi.intCast_apply

Modified Mathlib/Data/Nat/Cast/Pi.lean

deleted theorem Pi.natCast_apply