mk_all & lint

leanprover-community · Jul 3, 2024 · b02bab5 · b02bab5
1 parent aec5a8a
commit b02bab5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -600,6 +600,7 @@ import Mathlib.Algebra.Order.Ring.Prod
 import Mathlib.Algebra.Order.Ring.Rat
 import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Algebra.Order.Ring.Synonym
+import Mathlib.Algebra.Order.Ring.Unbundled.Basic
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Algebra.Order.Sub.Canonical

diff --git a/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean b/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
@@ -926,7 +926,7 @@ variable [ExistsAddOfLE α]
 /-- Binary **arithmetic mean-geometric mean inequality** (aka AM-GM inequality) for linearly ordered
 commutative semirings. -/
 lemma two_mul_le_add_sq [MulPosStrictMono α] [ContravariantClass α α (· + ·) (· ≤ ·)]
-  [CovariantClass α α (· + ·) (· ≤ ·)] (a b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
+    [CovariantClass α α (· + ·) (· ≤ ·)] (a b : α) : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
   simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul]
     using mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)
 #align two_mul_le_add_sq two_mul_le_add_sq