Commit 2024-09-08 04:56 ee90236e

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem NoZeroSMulDivisors.algebraMap_eq_one_iff

added theorem NoZeroSMulDivisors.algebraMap_eq_zero_iff

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

modified theorem RatFunc.algebraMap_eq_zero_iff

modified theorem RatFunc.algebraMap_ne_zero

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/NumberTheory/NumberField/Basic.lean

modified theorem NumberField.RingOfIntegers.coe_eq_zero_iff