Commit 2024-09-05 04:39 e5a9dc03

View on Github →

chore: split Analysis.Normed.Field.Basic (#16479)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/Normed/Field/Basic.lean

deleted theorem AddChar.norm_apply

deleted def DilationEquiv.mulLeft

deleted def DilationEquiv.mulRight

deleted theorem Filter.Tendsto.zero_mul_isBoundedUnder_le

deleted theorem Filter.comap_mul_left_cobounded

deleted theorem Filter.comap_mul_right_cobounded

deleted theorem Filter.inv_cobounded₀

deleted theorem Filter.inv_nhdsWithin_ne_zero

deleted theorem Filter.isBoundedUnder_le_mul_tendsto_zero

deleted theorem Filter.map_mul_left_cobounded

deleted theorem Filter.map_mul_right_cobounded

deleted theorem Filter.tendsto_inv₀_cobounded'

deleted theorem Filter.tendsto_inv₀_cobounded

deleted theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

deleted theorem Filter.tendsto_mul_left_cobounded

deleted theorem Filter.tendsto_mul_right_cobounded

deleted theorem NNReal.lipschitzWith_sub

deleted theorem NormedField.denseRange_nnnorm

deleted theorem antilipschitzWith_mul_left

deleted theorem antilipschitzWith_mul_right

Modified Mathlib/Analysis/Normed/Field/InfiniteSum.lean

Created Mathlib/Analysis/Normed/Field/Lemmas.lean

added theorem AddChar.norm_apply

added def DilationEquiv.mulLeft

added def DilationEquiv.mulRight

added theorem Filter.Tendsto.zero_mul_isBoundedUnder_le

added theorem Filter.comap_mul_left_cobounded

added theorem Filter.comap_mul_right_cobounded

added theorem Filter.inv_cobounded₀

added theorem Filter.inv_nhdsWithin_ne_zero

added theorem Filter.isBoundedUnder_le_mul_tendsto_zero

added theorem Filter.map_mul_left_cobounded

added theorem Filter.map_mul_right_cobounded

added theorem Filter.tendsto_inv₀_cobounded'

added theorem Filter.tendsto_inv₀_cobounded

added theorem Filter.tendsto_inv₀_nhdsWithin_ne_zero

added theorem Filter.tendsto_mul_left_cobounded

added theorem Filter.tendsto_mul_right_cobounded

added theorem NNReal.lipschitzWith_sub

added theorem NormedField.denseRange_nnnorm

added theorem antilipschitzWith_mul_left

added theorem antilipschitzWith_mul_right

Modified Mathlib/Analysis/Normed/Field/UnitBall.lean

Modified Mathlib/Analysis/Normed/Module/Basic.lean

Modified Mathlib/Analysis/Normed/MulAction.lean

Modified Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean

Modified Mathlib/Analysis/Normed/Order/Basic.lean

Modified Mathlib/Analysis/Normed/Ring/Seminorm.lean

Modified Mathlib/Analysis/NormedSpace/Int.lean

Modified Mathlib/Analysis/SumOverResidueClass.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/Ostrowski.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

Modified Mathlib/Topology/Bornology/BoundedOperation.lean

Modified Mathlib/Topology/MetricSpace/CauSeqFilter.lean

Modified Mathlib/Topology/MetricSpace/Polish.lean