From 4365b38f5a5c07fe225a4d3d331240c9f80fe770 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Mon, 6 Jan 2025 14:04:44 +0000 Subject: [PATCH] Add instances --- Mathlib/RingTheory/Etale/Pi.lean | 3 +++ Mathlib/RingTheory/Smooth/Pi.lean | 3 +++ Mathlib/RingTheory/Unramified/Pi.lean | 3 +++ 3 files changed, 9 insertions(+) diff --git a/Mathlib/RingTheory/Etale/Pi.lean b/Mathlib/RingTheory/Etale/Pi.lean index 12dc76f3f48d4..0e50eccd56627 100644 --- 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 index cfb4cf1dd16df..aab45da1545e8 100644 --- 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 index 755c16a601f58..ddebc82f3785d 100644 --- 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