Theorem Algebra.IsUnramifiedAt.of_restrictScalars

Modification history

2025-06-07 07:26

Mathlib/RingTheory/Unramified/Locus.lean

feat: connection between `Algebra.IsUnramifiedAt` and `Ideal.ramificationIdx`. (#25498)

Added Algebra.IsUnramifiedAt.of_restrictScalars View on Github →