Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-06 22:50
2f1f7b9c
View on Github →
feat: add @[simp] lemma Prod.norm_mk (
#20411
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Group/Constructions.lean
added
theorem
Prod.nnnorm_def'
added
theorem
Prod.nnnorm_mk'
deleted
theorem
Prod.nnorm_def
added
theorem
Prod.norm_mk
Modified
Mathlib/Analysis/Normed/Lp/ProdLp.lean
Modified
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
Modified
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean