Commit 2026-01-06 16:13 f9dae25d

View on Github →

refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp (#30706) This PR builds upon #8370 and avoids Algebra ℚ typeclass assumptions wherever possible. Many [NormedAlgebra ℚ 𝔸] can be generalized to [NontriviallyNormedField 𝕂] [CharZero 𝕂] [ContinuousSMul ℚ 𝕂] [NormedAlgebra 𝕂 𝔸], which basically means allowing ℚ to use other equivalent norms, and may not be the case of concern. It might be possible to use some Prop-valued typeclasses to avoid the diamond problem potentially caused by [NormedAlgebra ℚ 𝔸]. This makes it unnecessary to manually obtain [NormedAlgebra ℚ 𝔸] when we have [NormedAlgebra ℝ 𝔸] or [NormedAlgebra ℂ 𝔸].

Estimated changes

modified theorem DualNumber.exp_eps
modified theorem DualNumber.exp_smul_eps
modified theorem Commute.exp
modified theorem Commute.exp_left
modified theorem NormedSpace.exp_add
modified theorem NormedSpace.exp_analytic
modified theorem NormedSpace.exp_conj'
modified theorem NormedSpace.exp_conj
modified theorem NormedSpace.exp_continuous
deleted theorem NormedSpace.exp_eq_exp
modified theorem NormedSpace.exp_eq_tsum
modified theorem NormedSpace.exp_eq_tsum_div
modified theorem NormedSpace.exp_neg
modified theorem NormedSpace.exp_nsmul
modified theorem NormedSpace.exp_op
modified theorem NormedSpace.exp_sum
modified theorem NormedSpace.exp_units_conj'
modified theorem NormedSpace.exp_units_conj
modified theorem NormedSpace.exp_zero
modified theorem NormedSpace.exp_zsmul
modified theorem NormedSpace.invOf_exp
modified theorem NormedSpace.isUnit_exp
modified theorem NormedSpace.map_exp
modified theorem Prod.fst_exp
modified theorem Prod.snd_exp
modified theorem Ring.inverse_exp
modified theorem Matrix.IsSymm.exp
modified theorem Matrix.exp_blockDiagonal'
modified theorem Matrix.exp_blockDiagonal
modified theorem Matrix.exp_diagonal
modified theorem Matrix.exp_neg
modified theorem Matrix.exp_transpose
modified theorem Matrix.exp_zsmul
modified theorem Quaternion.exp_coe
modified theorem Quaternion.im_exp
modified theorem Quaternion.normSq_exp
modified theorem Quaternion.norm_exp
modified theorem Quaternion.re_exp
modified theorem spectrum.exp_mem_exp
modified theorem TrivSqZeroExt.exp_def
modified theorem TrivSqZeroExt.exp_inl
modified theorem TrivSqZeroExt.exp_inr
modified theorem TrivSqZeroExt.fst_exp
modified theorem TrivSqZeroExt.snd_exp
modified theorem CFC.log_exp
modified theorem IsSelfAdjoint.exp_nonneg
modified theorem Complex.exp_eq_exp_ℂ
modified theorem Real.exp_eq_exp_ℝ
modified theorem hasDerivAt_exp
modified theorem hasDerivAt_exp_of_mem_ball
modified theorem hasDerivAt_exp_zero
modified theorem hasFDerivAt_exp
modified theorem hasFDerivAt_exp_of_mem_ball
modified theorem hasFDerivAt_exp_zero
modified theorem hasStrictDerivAt_exp
modified theorem hasStrictDerivAt_exp_zero
modified theorem hasStrictFDerivAt_exp
modified theorem hasStrictFDerivAt_exp_zero