Commit 2024-04-29 15:46 e0235c08

View on Github →

chore(Data/Rat/Defs): Fix names of a few lemmas (#12505) There are more wrong lemmas in Std, but it's out of my scope

Estimated changes

Modified Mathlib/Algebra/Module/CharacterModule.lean

Modified Mathlib/Algebra/Order/Archimedean.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.coe_int_den

deleted theorem Rat.coe_int_num

added theorem Rat.den_intCast

modified theorem Rat.inv_mkRat

added theorem Rat.mk'_zero

deleted theorem Rat.mkRat_eq

added theorem Rat.mkRat_eq_divInt

modified theorem Rat.mkRat_one

deleted theorem Rat.mul_def'

added theorem Rat.mul_eq_mkRat

added theorem Rat.num_intCast

deleted theorem Rat.zero_mk

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/NumberTheory/DiophantineApproximation.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

Modified Mathlib/RingTheory/WittVector/StructurePolynomial.lean