Theorem Ideal.relNorm_comap_algEquiv

Modification history

2025-09-03 14:38
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat(Ideal): `relNorm` is preserved under the action of an `AlgEquiv` (#28724) …
Added Ideal.relNorm_comap_algEquivView on Github →