Commit 2024-04-21 07:28 ff9ef348

View on Github →

chore: make argument to sq_pos_of_ne_zero/sq_pos_iff implicit (#12288) This matches our general policy and zpow_two_pos_of_ne_zero. Also define sq_pos_of_ne_zero as an alias.

Estimated changes

Modified Mathlib/Algebra/GroupPower/Order.lean

modified theorem sq_pos_iff

deleted theorem sq_pos_of_ne_zero

Modified Mathlib/Algebra/Order/Chebyshev.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Combinatorics/Additive/Behrend.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/NumberTheory/FLT/Four.lean

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/Probability/Variance.lean