Theorems · Theorem · geometry

midpoint_sub_add

∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R (x - y) (x + y) = x

Defined in

Mathlib.LinearAlgebra.AffineSpace.Midpoint

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound

Assumes

RingInvertibleAddCommGroupModule