Theorem galLiftEquiv_algebraMap_apply

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 galLiftEquiv_algebraMap_applyView on Github →