Theorem galLift_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 galLift_idView on Github →