Commit 2024-11-25 11:42 f2336c4d

View on Github →

chore: delete lemmas about T0 seminormed groups (#19438) Those duplicate lemmas about normed groups

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

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

modified theorem norm_div_eq_zero_iff

deleted theorem norm_eq_zero'''

deleted theorem norm_eq_zero''

added theorem norm_eq_zero'

deleted theorem norm_le_zero_iff'''

deleted theorem norm_le_zero_iff''

added theorem norm_le_zero_iff'

modified theorem norm_ne_zero_iff'

deleted theorem norm_pos_iff'''

deleted theorem norm_pos_iff''

added theorem norm_pos_iff'

Modified Mathlib/Analysis/Normed/Group/Uniform.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified scripts/nolints_prime_decls.txt