Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-04-19 02:04
4e7ba671
View on Github →
feat(Analysis/SpecificLimits/Normed): generalize to division rings (
#12164
)
Estimated changes
Modified
Mathlib/Analysis/SpecificLimits/Normed.lean
modified
theorem
NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop
modified
theorem
NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop
modified
theorem
NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded
modified
theorem
hasSum_coe_mul_geometric_of_norm_lt_one
modified
theorem
tsum_coe_mul_geometric_of_norm_lt_one
Modified
Mathlib/Topology/ContinuousFunction/Units.lean
modified
theorem
ContinuousMap.isUnit_iff_forall_ne_zero
added
theorem
ContinuousMap.spectrum_eq_preimage_range
modified
theorem
ContinuousMap.spectrum_eq_range