Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.spanNorm_spanNorm_of_bot_or_top
Modification history
2025-08-22 16:49
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat(RingTheory/Ideal): prove transitivity for the relative norm (#27152) …
Added
Ideal.spanNorm_spanNorm_of_bot_or_top
View on Github →