Commit 2024-08-28 10:46 33d4a4af

View on Github →

chore(Pow/Real): fix lemma names about Nat.cast/Int.cast (#16214) From LeanAPAP

Estimated changes

deleted theorem Real.rpow_add_int'
deleted theorem Real.rpow_add_int
added theorem Real.rpow_add_intCast'
added theorem Real.rpow_add_intCast
deleted theorem Real.rpow_add_nat'
deleted theorem Real.rpow_add_nat
added theorem Real.rpow_add_natCast'
added theorem Real.rpow_add_natCast
deleted theorem Real.rpow_sub_int'
deleted theorem Real.rpow_sub_int
added theorem Real.rpow_sub_intCast'
added theorem Real.rpow_sub_intCast
deleted theorem Real.rpow_sub_nat'
deleted theorem Real.rpow_sub_nat
added theorem Real.rpow_sub_natCast'
added theorem Real.rpow_sub_natCast