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.