English
Red (invRev L1) (invRev L2) is equivalent to Red L1 L2.
Русский
Red (invRev L1) (invRev L2) эквивалентно Red L1 L2.
LaTeX
$$$Red\\,(invRev\\ L_1)\\,(invRev\\ L_2) \\iff Red\\ L_1\\ L_2$$$
Lean4
/-- If `β` is a group, then any function from `α` to `β` extends uniquely to a group homomorphism
from the free group over `α` to `β` -/
@[to_additive (attr := simps symm_apply) /--
If `β` is an additive group, then any function from `α` to `β` extends uniquely to an
additive group homomorphism from the free additive group over `α` to `β` -/
]
def lift : (α → β) ≃ (FreeGroup α →* β)
where
toFun f := MonoidHom.mk' (Quot.lift (Lift.aux f) fun _ _ => Red.Step.lift) <| by rintro ⟨L₁⟩ ⟨L₂⟩; simp [Lift.aux]
invFun g := g ∘ of
left_inv f := List.prod_singleton
right_inv g := by ext; simp [of, Lift.aux]
