Missing derived operations in Algebra.Structures.IsGroup
/Algebra.Bundles.Raw.RawGroup
#2268
Labels
Algebra.Structures.IsGroup
/Algebra.Bundles.Raw.RawGroup
#2268
y ∙ x ∙ (y ⁻¹)
,(y ⁻¹) ∙ x ∙ y
; (obviously interdefinable, but at the cost of having to repeatedly invoke⁻¹-involutive
)y ∙ x ∙ (y ⁻¹) ∙ (x ⁻¹)
,(x ⁻¹) ∙ (y ⁻¹) ∙ x ∙ y
; (ditto.)x ∙ (y ⁻¹) ∙ z
;where, in each case, we have to choose a suitable bracketing... Plus... properties?
Outstanding issue from #2252 , #2247 / #2251 : where should these new operations live?
The text was updated successfully, but these errors were encountered: