Commit 2024-08-16 09:35 3913a5ee

View on Github →

feat(NNRat): More basic lemmas (#15047) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Algebra/Rat.lean

added theorem NNRat.cast_smul_eq_nnqsmul

added theorem Rat.cast_smul_eq_qsmul

modified theorem algebraMap_rat_rat

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

Modified Mathlib/Data/NNRat/Defs.lean

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

added def NNRat.castHom

added theorem NNRat.cast_add

added theorem NNRat.cast_div

added theorem NNRat.cast_divNat

added theorem NNRat.cast_eq_zero

added theorem NNRat.cast_inj

added theorem NNRat.cast_injective

added theorem NNRat.cast_inv

added theorem NNRat.cast_mul

added theorem NNRat.cast_ne_zero

added theorem NNRat.cast_zpow

added theorem NNRat.coe_castHom

modified theorem Rat.cast_add

modified theorem Rat.cast_div

modified theorem Rat.cast_eq_zero

modified theorem Rat.cast_inj

modified theorem Rat.cast_injective

modified theorem Rat.cast_inv

modified theorem Rat.cast_mul

modified theorem Rat.cast_ne_zero

deleted theorem Rat.cast_pow

modified theorem Rat.cast_sub

modified theorem Rat.cast_zpow

added theorem Rat.coe_castHom

deleted theorem Rat.coe_cast_hom

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

deleted theorem MonoidWithZeroHom.ext_rat'

deleted theorem MonoidWithZeroHom.ext_rat

deleted theorem MonoidWithZeroHom.ext_rat_on_pnat

added theorem MonoidWithZeroHomClass.ext_nnrat'

added theorem MonoidWithZeroHomClass.ext_nnrat

added theorem MonoidWithZeroHomClass.ext_nnrat_on_pnat

added theorem MonoidWithZeroHomClass.ext_rat'

added theorem MonoidWithZeroHomClass.ext_rat

added theorem MonoidWithZeroHomClass.ext_rat_on_pnat

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

added theorem Rat.cast_pow

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified test/TCSynth.lean

Created test/instance_diamonds/algebra_rat.lean