pith. machine review for the scientific record. sign in
theorem proved tactic proof

shiftedCompose_val

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 238@[simp] theorem shiftedCompose_val (A B : ShiftedCarrier) :
 239    ((A * B : ShiftedCarrier) : ℝ) = 2 * A.1 * B.1 := rfl

proof body

Tactic-mode proof.

 240
 241noncomputable instance : CommMonoid ShiftedCarrier where
 242  mul := (· * ·)
 243  mul_assoc A B C := by
 244    apply Subtype.ext
 245    change 2 * (2 * A.1 * B.1) * C.1 = 2 * A.1 * (2 * B.1 * C.1)
 246    ring
 247  one := 1
 248  one_mul A := by
 249    apply Subtype.ext
 250    change 2 * (1 / 2 : ℝ) * A.1 = A.1
 251    ring
 252  mul_one A := by
 253    apply Subtype.ext
 254    change 2 * A.1 * (1 / 2 : ℝ) = A.1
 255    ring
 256  mul_comm A B := by
 257    apply Subtype.ext
 258    change 2 * A.1 * B.1 = 2 * B.1 * A.1
 259    ring
 260
 261/-- `H(x)` lands in `[1, ∞)` on positive reals, hence in `[1/2, ∞)` as well. -/

depends on (17)

Lean names referenced from this declaration's body.