Commit 2026-08-13 17:23 1de9bcbf
View on Github →refactor(RingTheory/IntegralClosure/IsIntegral/Basic): use FaithfulSMul in isIntegral_algebraMap_iff (#41291)
Currently isIntegral_algebraMap_iff takes an explicit assumption stating that algebraMap A B is nonzero, but a [FaithfulSMul A B] typeclass is more idiomatic (and can almost always be inferred automatically).