Commit 2025-02-03 14:49 3e6a2f15

View on Github →

feat: generalise algebraMap_injective by weakening its typeclass assumptions (#21287) As shown in the new lemma faithfulSMul_iff_algebraMap_injective, injectivity of algebraMap R A is equivalent to the typeclass hypothesis [FaithfulSMul R A]. We thus generalise (and rename) the existing lemma NoZeroSMulDivisors.algebraMap_injective to FaithfulSMul.algebraMap_injective. The rename is responsible for much of the diff. By weakening the assumptions [Nontrivial A] [NoZeroSMulDivisors R A] to just [FaithfulSMul R A], results which need to use algebraMap_injective can be applied in the case that we have [Ring A] [CharZero A] but fail to have [NoZeroSMulDivisors ℤ A]. This is the motivation for these changes. There are quite a few places in the library where a lemma consumes an explicit argument of the form Injective (algebraMap R A). Most / all of these should probably be restated to accept the typeclass argument [FaithfulSMul R A] but we do not attempt such a refactor here.

Estimated changes