Theorem integralClosure.coe_smul

Modification history

2025-11-09 18:05
Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean
refactor(NumberTheory/RamificationInertia/Galois): switch to `IsGaloisGroup G A B` (#30934) …
Added integralClosure.coe_smulView on Github →