## Stream: maths

### Topic: one_iff_ker_inv

#### Kevin Buzzard (Mar 02 2019 at 14:08):

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 (Mar 02 2019 at 14:08):

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

Last updated: May 11 2021 at 15:12 UTC