English
There is a dual induction principle for closure using right-multiplication by generators.
Русский
Существует двойственный индукционный принцип по замыканию через правое умножение на образующие.
LaTeX
$$closure_induction_right ... p x h$$
Lean4
/-- For subgroups generated by a single element, see the simpler `zpow_induction_right`. -/
@[to_additive (attr := elab_as_elim) /-- For additive subgroups generated by a single element, see the simpler
`zsmul_induction_right`. -/
]
theorem closure_induction_right {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
(mul_right : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
(mul_inv_cancel : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y⁻¹) (mul_mem hx (inv_mem (subset_closure hy))))
{x : G} (h : x ∈ closure s) : p x h :=
closure_induction_left (s := MulOpposite.unop ⁻¹' s) (p := fun m hm => p m.unop <| by rwa [← op_closure] at hm) one
(fun _x hx _y _ => mul_right _ _ _ hx) (fun _x hx _y _ => mul_inv_cancel _ _ _ hx) (by rwa [← op_closure])
