Commit 2024-07-16 12:01 2eda6f48

View on Github →

chore: unify add_halves and add_halves' (#14790) by generalizing to DivisionSemiring

Estimated changes

Modified Counterexamples/Pseudoelement.lean

Modified Mathlib/Algebra/CharZero/Lemmas.lean

deleted theorem add_halves'

added theorem add_halves

added theorem add_self_div_two

deleted theorem half_add_self

modified theorem sub_half

Modified Mathlib/Algebra/Order/Field/Basic.lean

deleted theorem add_halves

deleted theorem add_self_div_two

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Data/Complex/Exponential.lean

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean