We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 862abe4 commit 2d799b9Copy full SHA for 2d799b9
2 files changed
Mathlib/Analysis/Convex/Basic.lean
@@ -641,5 +641,3 @@ lemma convex_of_nonneg_surjective_algebraMap [FaithfulSMul R A] {s : Set M}
641
exact (FaithfulSMul.algebraMap_eq_one_iff R A).mp hab
642
643
end CommSemiring
644
-
645
-#min_imports
Mathlib/Analysis/LocallyConvex/Basic.lean
@@ -314,5 +314,3 @@ theorem balanced_iff_neg_mem (hs : Convex ℝ s) : Balanced ℝ s ↔ ∀ ⦃x
314
(div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)
315
316
end Real
317
318
0 commit comments