Theorems · Definition · geometry
Projectivization.orthogonal
{F : Type u_1} →
[inst : Field F] → {m : Type u_2} → [Fintype m] → Projectivization F (m → F) → Projectivization F (m → F) → PropOrthogonality on the projective plane.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Fieldstatement and proof · cited by 7,404
- dotProductproof · cited by 194
- Projectivizationstatement · cited by 111
Cited by10
Results whose statement or proof uses this declaration.
- Projectivization.cross_orthogonal_leftstatement and proof · cited by 2
- Projectivization.orthogonal_commstatement and proof · cited by 2
- Projectivization.orthogonal_mkstatement · cited by 2
- Projectivization.cross_orthogonal_rightstatement and proof · cited by 1
- Projectivization.exists_not_self_orthogonalstatement · cited by 1
- Projectivization.orthogonal_cross_rightstatement · cited by 0
- Configuration.ofField.eq_or_eq_of_orthogonalstatement and proof · cited by 0
- Configuration.ofField.mem_iffstatement · cited by 0
- Projectivization.orthogonal_cross_leftstatement · cited by 0
- Projectivization.exists_not_orthogonal_selfstatement · cited by 0