Commit 2024-02-13 19:40 3cb73aef

View on Github →

chore: Move lemmas about Function.const to the Function namespace (#10220) They were in the Pi namespace instead.

Estimated changes

Modified Mathlib/Algebra/Order/Pi.lean

Modified Mathlib/Data/Pi/Algebra.lean

added theorem Function.const_div

added theorem Function.const_inv

added theorem Function.const_mul

added theorem Function.const_one

added theorem Function.const_pow

deleted theorem Pi.const_div

deleted theorem Pi.const_inv

deleted theorem Pi.const_mul

deleted theorem Pi.const_one

deleted theorem Pi.const_pow

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/Probability/StrongLaw.lean