Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-26 20:16
434a749a
View on Github →
chore: rename round_add_int and related declarations (
#23234
)
Estimated changes
Modified
Mathlib/Algebra/Order/Round.lean
deleted
theorem
round_add_int
added
theorem
round_add_intCast
deleted
theorem
round_add_nat
added
theorem
round_add_natCast
added
theorem
round_intCast_add
deleted
theorem
round_int_add
added
theorem
round_natCast_add
deleted
theorem
round_nat_add
deleted
theorem
round_sub_int
added
theorem
round_sub_intCast
deleted
theorem
round_sub_nat
added
theorem
round_sub_natCast