Theorem galRestrict'_id

Modification history

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