Theorem NoZeroSMulDivisors.algebraMap_eq_one_iff

Modification history

2024-09-08 04:56

Mathlib/Algebra/Algebra/Basic.lean

feat(Algebra/Algebra/Basic): prove `algebraMap_eq_zero_iff` for `NoZeroSMulDivisors` (#16582)

Added NoZeroSMulDivisors.algebraMap_eq_one_iff View on Github →