Add instances

leanprover-community · Jan 6, 2025 · 4365b38 · 4365b38
1 parent 4af89a0
commit 4365b38
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 0 deletions.
diff --git a/Mathlib/RingTheory/Etale/Pi.lean b/Mathlib/RingTheory/Etale/Pi.lean
@@ -30,4 +30,7 @@ theorem pi_iff [Finite I] :
   simp_rw [FormallyEtale.iff_unramified_and_smooth, forall_and]
   rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]
 
+instance [Finite I] [∀ i, FormallyEtale R (A i)] : FormallyEtale R (Π i, A i) :=
+  .of_unramified_and_smooth
+
 end Algebra.FormallyEtale
diff --git a/Mathlib/RingTheory/Smooth/Pi.lean b/Mathlib/RingTheory/Smooth/Pi.lean
@@ -118,4 +118,7 @@ theorem pi_iff [Finite I] :
       rwa [mul_sub, ← map_mul, mul_comm, mul_assoc, (he.idem i).eq, he', ← map_mul, ← Pi.single_mul,
         one_mul, sub_eq_zero] at this
 
+instance [Finite I] [∀ i, FormallySmooth R (A i)] : FormallySmooth R (Π i, A i) :=
+  (pi_iff _).mpr ‹_›
+
 end Algebra.FormallySmooth
diff --git a/Mathlib/RingTheory/Unramified/Pi.lean b/Mathlib/RingTheory/Unramified/Pi.lean
@@ -95,4 +95,7 @@ theorem pi_iff :
         Ideal.Quotient.mkₐ_eq_mk]
       exact Ideal.mem_map_of_mem (Ideal.Quotient.mk J') (hf (Pi.single x r))
 
+instance [∀ i, FormallyUnramified R (f i)] : FormallyUnramified R (Π i, f i) :=
+  (pi_iff _).mpr ‹_›
+
 end Algebra.FormallyUnramified