Commit 2026-09-28 20:18 294c41f3

View on Github →

chore: rename nnorm to nnnorm in declaration names (#44290) Rename nnorm to nnnorm in Complex.conjCLE_nnorm and LipschitzWith.nnorm_le_mul(′).

Estimated changes

Modified Mathlib/Analysis/Complex/OperatorNorm.lean

added theorem Complex.conjCLE_nnnorm

deleted theorem Complex.conjCLE_nnorm

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

added theorem LipschitzWith.nnnorm_le_mul'

deleted theorem LipschitzWith.nnorm_le_mul'

Modified scripts/nolints_prime_decls.txt