Commit 2024-12-30 10:07 c4263a50
View on Github →chore: Rename injectivity theorems for consistency (#20329) Moves: Subgroup.toSubmonoid_eq -> Subgroup.toSubmonoid_inj AddSubgroup.toAddSubmonoid_eq -> AddSubgroup.toAddSubmonoid_inj Submodule.toAddSubmonoid_eq -> Submodule.toAddSubmonoid_inj Submodule.toAddSubgroup_eq -> Submodule.toAddSubgroup_inj Submodule.toSubMulAction_eq -> Submodule.toSubMulAction_inj Cardinal.toNat_eq_iff_eq_of_lt_aleph0 -> Cardinal.toNat_inj_of_lt_aleph0 IntermediateField.toSubalgebra_eq_iff -> IntermediateField.toSubalgebra_inj NormedSpace.Dual.toWeakDual_eq_iff -> NormedSpace.Dual.toWeakDual_inj WeakDual.toNormedDual_eq_iff -> WeakDual.toNormedDual_inj RatFunc.toFractionRing_eq_iff -> RatFunc.toFractionRing_inj Cardinal.toPartENat_eq_iff_of_le_aleph0 -> Cardinal.toPartENat_inj_of_le_aleph0 ENat.toENNReal_coe_eq_iff -> ENat.toENNReal_coe_inj Ordinal.toGame_eq_iff -> Ordinal.toGame_inj Ordinal.toPGame_eq_iff -> Ordinal.toPGame_inj DirichletCharacter.toUnitHom_eq_iff -> DirichletCharacter.toUnitHom_inj LieSubalgebra.coe_to_submodule_eq_iff -> LieSubalgebra.coe_to_submodule_inj LieSubmodule.coe_toSubmodule_eq_iff -> LieSubmodule.coe_toSubmodule_inj