one_iff_ker_inv

Stream: maths

[Kevin Buzzard]

The equivalence relation used when defining quotient groups is λ x y, x⁻¹ * y ∈ <subgroup>. But lemmas like one_iff_ker_inv in subgroup.lean are stated in the form f a = f b ↔ f (a * b⁻¹) = 1 with the inverse on the right. Are lemmas such as f a = f b ↔ f (a⁻¹ * b) = 1 in mathlib? If not, what is a suitable name for them? one_iff_ker_inv'?

[Kevin Buzzard]

PS backtick stuff doesn't work in links, apparently.