Theorem Algebra.intNorm_map_algEquiv

Modification history

2025-12-07 22:48

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

chore(RingTheory): generalize `Algebra.intNorm` (#32542) …

Modified Algebra.intNorm_map_algEquiv View on Github →

2025-09-03 14:38

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

feat(Ideal): `relNorm` is preserved under the action of an `AlgEquiv` (#28724) …

Added Algebra.intNorm_map_algEquiv View on Github →