Theorem IsIntegralClosure.faithfulSMul

Modification history

2026-08-13 17:23

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Defs.lean

refactor(RingTheory/IntegralClosure/IsIntegral/Basic): use `FaithfulSMul` in `isIntegral_algebraMap_iff` (#41291) …

Added IsIntegralClosure.faithfulSMul View on Github →