Theorem TrivSqZeroExt.fst_exp

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.fst_exp View on Github →

2023-06-03 12:15

Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean

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

Added TrivSqZeroExt.fst_exp View on Github →