We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b4470de commit 39dacb0Copy full SHA for 39dacb0
Mathlib/Geometry/Euclidean/Incenter.lean
@@ -699,7 +699,7 @@ lemma ExcenterExists.affineSpan_faceOpposite_eq_orthRadius [hf : Fact (Module.fi
699
rw [direction_affineSpan, (s.faceOpposite i).independent.finrank_vectorSpan_add_one,
700
Fintype.card_fin, hf.out]
701
have := NeZero.ne n
702
- cutsat
+ lia
703
704
lemma affineSpan_faceOpposite_eq_orthRadius_insphere [Fact (Module.finrank ℝ V = n)]
705
(i : Fin (n + 1)) :
0 commit comments