noncomputable def unitInterval.assocProd (p q : ↑unitInterval) : ↑unitInterval

Helper function for choose_assoc

Equations

• unitInterval.assocProd p q = ⟨↑(unitInterval.symm p) * ↑q / ↑(unitInterval.symm (p * q)), ⋯⟩

@[simp]

theorem unitInterval.assocProd_coe (p q : ↑unitInterval) : ↑(assocProd p q) = ↑(symm p) * ↑q / ↑(symm (p * q))

def unitInterval.«term_⍟_» : Lean.TrailingParserDescr

Helper function for choose_assoc

Equations

• unitInterval.«term_⍟_» = Lean.ParserDescr.trailingNode `unitInterval.«term_⍟_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⍟ ") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem unitInterval.mul_assocProd (p q : ↑unitInterval) : symm (p * q) * assocProd p q = symm p * q

@[simp]

theorem unitInterval.mul_symm_assocProd (p q : ↑unitInterval) : symm (p * q) * symm (assocProd p q) = symm q

@[simp]

theorem unitInterval.mul_symm_assocProd' (p q : ↑unitInterval) (hpq : p < 1 ∨ q < 1) : p * symm (assocProd p q) = assocProd q p