Theorem TrivSqZeroExt.exp_inr

Modification history

2026-01-06 16:13

Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` (#30706) …

Modified TrivSqZeroExt.exp_inr View on Github →

2023-06-03 12:15

Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean

feat: port Analysis.NormedSpace.TrivSqZeroExt (#4626)

Added TrivSqZeroExt.exp_inr View on Github →