English
If G is a DivisionMonoid, then Germ l G is a DivisionMonoid, with operations induced pointwise from G.
Русский
Если G имеется как делив-монойд, то Germ l G также является делив-монойдом, операции которого получены покомпонентно из G.
LaTeX
$$$ \\mathrm{Germ}(l,G) \\text{ is a DivisionMonoid, with } \\operatorname{div}_{\\mathrm{Germ}}(x,y) = \\mathrm{Germ}(\\operatorname{div}_G)(x,y). $$$
Lean4
@[to_additive subNegMonoid]
instance instDivInvMonoid [DivInvMonoid G] : DivInvMonoid (Germ l G)
where
zpow z f := f ^ z
zpow_zero' := Quotient.ind' fun _ => congrArg ofFun <| funext fun _ => DivInvMonoid.zpow_zero' _
zpow_succ' _ := Quotient.ind' fun _ => congrArg ofFun <| funext fun _ => DivInvMonoid.zpow_succ' ..
zpow_neg' _ := Quotient.ind' fun _ => congrArg ofFun <| funext fun _ => DivInvMonoid.zpow_neg' ..
div_eq_mul_inv := Quotient.ind₂' fun _ _ ↦ congrArg ofFun <| div_eq_mul_inv ..
