Nuprl Definition : line-det
line-det(a;b;c;d) ==
((((d 1) * (a 1)) - (d 1) * (a 0) - (d 0) * (a 1)) + ((d 0) * (a 0))) - (((b 1) * (c 1)) - (b 1) * (c 0) - (b 0)
* (c 1))
+ ((b 0) * (c 0))
Definitions occuring in Statement :
rsub: x - y,
rmul: a * b,
radd: a + b,
apply: f a,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
apply: f a,
rmul: a * b,
rsub: x - y,
radd: a + b
FDL editor aliases :
line-det
Latex:
line-det(a;b;c;d) ==
((((d 1) * (a 1)) - (d 1) * (a 0) - (d 0) * (a 1)) + ((d 0) * (a 0))) - (((b 1) * (c 1)) - (b 1)
* (c 0) - (b 0) * (c 1))
+ ((b 0) * (c 0))
Date html generated:
2018_07_29-AM-09_47_05
Last ObjectModification:
2018_07_02-PM-03_05_24
Theory : reals!model!euclidean!geometry
Home
Index