Commit 2024-11-18 16:51 9c84692f

View on Github →

chore: Split Mathlib.RingTheory.Ideal.Norm (#19211) We split Mathlib.RingTheory.Ideal.Norm into Basic and RelNorm. This is in preparation to generalize Ideal.RelNorm to nonfree extensions.

Estimated changes

deleted theorem Ideal.map_relNorm
deleted theorem Ideal.map_spanNorm
deleted theorem Ideal.norm_mem_relNorm
deleted theorem Ideal.norm_mem_spanNorm
deleted def Ideal.relNorm
deleted theorem Ideal.relNorm_apply
deleted theorem Ideal.relNorm_bot
deleted theorem Ideal.relNorm_eq_bot_iff
deleted theorem Ideal.relNorm_mono
deleted theorem Ideal.relNorm_singleton
deleted theorem Ideal.relNorm_top
deleted def Ideal.spanNorm
deleted theorem Ideal.spanNorm_bot
deleted theorem Ideal.spanNorm_eq
deleted theorem Ideal.spanNorm_eq_bot_iff
deleted theorem Ideal.spanNorm_mono
deleted theorem Ideal.spanNorm_mul
deleted theorem Ideal.spanNorm_singleton
deleted theorem Ideal.spanNorm_top
added theorem Ideal.map_relNorm
added theorem Ideal.map_spanNorm
added theorem Ideal.norm_mem_relNorm
added def Ideal.relNorm
added theorem Ideal.relNorm_apply
added theorem Ideal.relNorm_bot
added theorem Ideal.relNorm_mono
added theorem Ideal.relNorm_top
added def Ideal.spanNorm
added theorem Ideal.spanNorm_bot
added theorem Ideal.spanNorm_eq
added theorem Ideal.spanNorm_mono
added theorem Ideal.spanNorm_mul
added theorem Ideal.spanNorm_top