Mathlib Map

Theorems · Theorem · geometry

AffineMap.lineMap_apply_ring

∀ {k : Type u_1} [inst : Ring k] (a b c : k), (AffineMap.lineMap a b) c = (1 - c) * a + c * b
Defined in
Mathlib.LinearAlgebra.AffineSpace.AffineMap
Cited by
2 results in Mathlib
Foundations
Depth 46 from the axioms · uses propext, Quot.sound
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

wbtw_zero_one_iff · cited by 2wbtw_zero_one_ifflineMap_slope_lineMap_slope_lineMap · cited by 1lineMap_slope_lineMap_slo…DFunLike.coe · cited by 62936DFunLike.coeRing · cited by 7463RingAffineMap · cited by 674AffineMapAffineMap.lineMap · cited by 254AffineMap.lineMapAffineMap.lineMap_apply_module · cited by 16AffineMap.lineMap_apply_m…AffineMap.lineMap_apply_ringCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.