Theorem Real.exp_one_pow

Modification history

2024-04-17 11:15

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …

Modified Real.exp_one_pow View on Github →

2023-12-19 15:21

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

feat: More `rpow` lemmas (#9108) …

Added Real.exp_one_pow View on Github →