English
An equivalent formulation: f is injective iff f(a) = 1 implies a = 1, equivalently f(a) = f(b) implies a = b when restricted to the kernel.
Русский
Эквивалентная формулировка: f инъективен тогда, когда f(a) = 1 ⇒ a = 1; эквивалентно: f(a) = f(b) ⇒ a = b на каноне.
LaTeX
$$$\operatorname{Injective}(f) \iff \forall a, f(a) = 1 \iff a = 1$$$
Lean4
/-- Makes a group homomorphism from a proof that the map preserves right division
`fun x y => x * y⁻¹`. See also `MonoidHom.of_map_div` for a version using `fun x y => x / y`.
-/
@[to_additive /-- Makes an additive group homomorphism from a proof that the map preserves
the operation `fun a b => a + -b`. See also `AddMonoidHom.ofMapSub` for a version using
`fun a b => a - b`. -/
]
def ofMapMulInv {H : Type*} [Group H] (f : G → H) (map_div : ∀ a b : G, f (a * b⁻¹) = f a * (f b)⁻¹) : G →* H :=
(mk' f) fun x y =>
calc
f (x * y) = f x * (f <| 1 * 1⁻¹ * y⁻¹)⁻¹ := by { simp only [one_mul, inv_one, ← map_div, inv_inv]
}
_ = f x * f y := by {
simp only [map_div]
simp only [mul_inv_cancel, one_mul, inv_inv]
}
