Theorem NoZeroSMulDivisors.algebraMap_eq_zero_iff

Modification history

2025-02-03 14:49
Mathlib/Algebra/Algebra/Basic.lean
feat: generalise `algebraMap_injective` by weakening its typeclass assumptions (#21287) …
Deleted NoZeroSMulDivisors.algebraMap_eq_zero_iffView on Github →
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_zero_iffView on Github →