From 0980052c7ca3d88a910949d0549f72db721870df Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 2 Aug 2024 07:08:50 +0000 Subject: [PATCH] chore: backports for leanprover/lean4#4814 (part 13) (#15397) see https://github.com/leanprover-community/mathlib4/pull/15245 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> --- Mathlib/Algebra/Order/Antidiag/Finsupp.lean | 2 +- Mathlib/CategoryTheory/Galois/Basic.lean | 32 ++++++---- Mathlib/Data/Nat/Choose/Multinomial.lean | 4 +- Mathlib/GroupTheory/Abelianization.lean | 11 ++-- Mathlib/GroupTheory/GroupAction/Basic.lean | 2 +- Mathlib/GroupTheory/GroupAction/Quotient.lean | 4 +- Mathlib/GroupTheory/NoncommPiCoprod.lean | 38 ++++++------ Mathlib/GroupTheory/OrderOfElement.lean | 60 ++++++++++--------- Mathlib/GroupTheory/Perm/Cycle/Factors.lean | 25 ++++---- Mathlib/GroupTheory/PresentedGroup.lean | 15 +++-- Mathlib/SetTheory/Cardinal/Ordinal.lean | 11 ++-- Mathlib/SetTheory/Surreal/Multiplication.lean | 23 ++++--- Mathlib/Topology/Bases.lean | 23 +++---- Mathlib/Topology/Clopen.lean | 12 ++-- scripts/style-exceptions.txt | 1 + 15 files changed, 145 insertions(+), 118 deletions(-) diff --git a/Mathlib/Algebra/Order/Antidiag/Finsupp.lean b/Mathlib/Algebra/Order/Antidiag/Finsupp.lean index 555a5dcbcaf32..05c533be79868 100644 --- a/Mathlib/Algebra/Order/Antidiag/Finsupp.lean +++ b/Mathlib/Algebra/Order/Antidiag/Finsupp.lean @@ -83,7 +83,7 @@ theorem mem_finsuppAntidiag_insert {a : ι} {s : Finset ι} intro x hx rw [update_noteq (ne_of_mem_of_not_mem hx h) n1 ⇑g] -theorem finsuppAntidiag_insert [DecidableEq μ] {a : ι} {s : Finset ι} +theorem finsuppAntidiag_insert {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) : finsuppAntidiag (insert a s) n = (antidiagonal n).biUnion (fun p : μ × μ => diff --git a/Mathlib/CategoryTheory/Galois/Basic.lean b/Mathlib/CategoryTheory/Galois/Basic.lean index a7a04b9c5a54e..60874987826dd 100644 --- a/Mathlib/CategoryTheory/Galois/Basic.lean +++ b/Mathlib/CategoryTheory/Galois/Basic.lean @@ -106,6 +106,7 @@ class PreservesIsConnected {C : Type u₁} [Category.{u₂, u₁} C] {D : Type v /-- `F.obj X` is connected if `X` is connected. -/ preserves : ∀ {X : C} [IsConnected X], IsConnected (F.obj X) +section variable {C : Type u₁} [Category.{u₂, u₁} C] [PreGaloisCategory C] attribute [instance] hasTerminal hasPullbacks hasFiniteCoproducts hasQuotientsByFiniteGroups @@ -116,6 +117,8 @@ instance : HasBinaryProducts C := hasBinaryProducts_of_hasTerminal_and_pullbacks instance : HasEqualizers C := hasEqualizers_of_hasPullbacks_and_binary_products +end + namespace FiberFunctor variable {C : Type u₁} [Category.{u₂, u₁} C] {F : C ⥤ FintypeCat.{w}} [PreGaloisCategory C] @@ -156,7 +159,8 @@ instance : F.Faithful where end FiberFunctor -variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F] +variable {C : Type u₁} [Category.{u₂, u₁} C] + (F : C ⥤ FintypeCat.{w}) /-- The canonical action of `Aut F` on the fiber of each object. -/ instance (X : C) : MulAction (Aut F) (F.obj X) where @@ -168,6 +172,20 @@ lemma mulAction_def {X : C} (σ : Aut F) (x : F.obj X) : σ • x = σ.hom.app X x := rfl +/-- An object that is neither initial or connected has a non-trivial subobject. -/ +lemma has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬ IsConnected X) + (hi : IsInitial X → False) : + ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬ IsIso v) := by + contrapose! hc + exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩ + +/-- The cardinality of the fiber is preserved under isomorphisms. -/ +lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y) := by + have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i) + exact Nat.card_eq_of_bijective e (Equiv.bijective e) + +variable [PreGaloisCategory C] [FiberFunctor F] + /-- An object is initial if and only if its fiber is empty. -/ lemma initial_iff_fiber_empty (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (F.obj X) := by rw [(IsInitial.isInitialIffObj F X).nonempty_congr] @@ -189,13 +207,6 @@ lemma not_initial_iff_fiber_nonempty (X : C) : (IsInitial X → False) ↔ Nonem lemma not_initial_of_inhabited {X : C} (x : F.obj X) (h : IsInitial X) : False := ((initial_iff_fiber_empty F X).mp ⟨h⟩).false x -/-- An object that is neither initial or connected has a non-trivial subobject. -/ -lemma has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬ IsConnected X) - (hi : IsInitial X → False) : - ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬ IsIso v) := by - contrapose! hc - exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩ - /-- The fiber of a connected object is nonempty. -/ instance nonempty_fiber_of_isConnected (X : C) [IsConnected X] : Nonempty (F.obj X) := by by_contra h @@ -339,11 +350,6 @@ lemma card_fiber_coprod_eq_sum (X Y : C) : rw [← Nat.card_sum] exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e) -/-- The cardinality of the fiber is preserved under isomorphisms. -/ -lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y) := by - have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i) - exact Nat.card_eq_of_bijective e (Equiv.bijective e) - /-- The cardinality of morphisms `A ⟶ X` is smaller than the cardinality of the fiber of the target if the source is connected. -/ lemma card_hom_le_card_fiber_of_connected (A X : C) [IsConnected A] : diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean index ea2ca2758b724..f41552ee482ec 100644 --- a/Mathlib/Data/Nat/Choose/Multinomial.lean +++ b/Mathlib/Data/Nat/Choose/Multinomial.lean @@ -249,7 +249,7 @@ lemma sum_pow_eq_sum_piAntidiag_of_commute (s : Finset α) (f : α → R) exact ne_of_mem_of_not_mem ht has /-- The **multinomial theorem**. -/ -theorem sum_pow_of_commute [Semiring R] (x : α → R) (s : Finset α) +theorem sum_pow_of_commute (x : α → R) (s : Finset α) (hc : (s : Set α).Pairwise fun i j => Commute (x i) (x j)) : ∀ n, s.sum x ^ n = @@ -297,7 +297,7 @@ lemma sum_pow_eq_sum_piAntidiag (s : Finset α) (f : α → R) (n : ℕ) : simp_rw [← noncommProd_eq_prod] rw [← sum_pow_eq_sum_piAntidiag_of_commute _ _ fun _ _ _ _ _ ↦ Commute.all ..] -theorem sum_pow [CommSemiring R] (x : α → R) (n : ℕ) : +theorem sum_pow (x : α → R) (n : ℕ) : s.sum x ^ n = ∑ k ∈ s.sym n, k.val.multinomial * (k.val.map x).prod := by conv_rhs => rw [← sum_coe_sort] convert sum_pow_of_commute x s (fun _ _ _ _ _ ↦ Commute.all ..) n diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean index ea8ee404b3876..0b848d11ae3ab 100644 --- a/Mathlib/GroupTheory/Abelianization.lean +++ b/Mathlib/GroupTheory/Abelianization.lean @@ -188,10 +188,10 @@ end Abelianization section AbelianizationCongr -- Porting note: `[Group G]` should not be necessary here -variable {G} [Group G] {H : Type v} [Group H] (e : G ≃* H) +variable {G} {H : Type v} [Group H] /-- Equivalent groups have equivalent abelianizations -/ -def MulEquiv.abelianizationCongr : Abelianization G ≃* Abelianization H where +def MulEquiv.abelianizationCongr (e : G ≃* H) : Abelianization G ≃* Abelianization H where toFun := Abelianization.map e.toMonoidHom invFun := Abelianization.map e.symm.toMonoidHom left_inv := by @@ -203,7 +203,7 @@ def MulEquiv.abelianizationCongr : Abelianization G ≃* Abelianization H where map_mul' := MonoidHom.map_mul _ @[simp] -theorem abelianizationCongr_of (x : G) : +theorem abelianizationCongr_of (e : G ≃* H) (x : G) : e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x) := rfl @@ -213,11 +213,12 @@ theorem abelianizationCongr_refl : MulEquiv.toMonoidHom_injective Abelianization.lift_of @[simp] -theorem abelianizationCongr_symm : e.abelianizationCongr.symm = e.symm.abelianizationCongr := +theorem abelianizationCongr_symm (e : G ≃* H) : + e.abelianizationCongr.symm = e.symm.abelianizationCongr := rfl @[simp] -theorem abelianizationCongr_trans {I : Type v} [Group I] (e₂ : H ≃* I) : +theorem abelianizationCongr_trans {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) : e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr := MulEquiv.toMonoidHom_injective (Abelianization.hom_ext _ _ rfl) diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index e106389c6b30d..a9941862041dd 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/Mathlib/GroupTheory/GroupAction/Basic.lean @@ -661,7 +661,7 @@ lemma stabilizer_smul_eq_left [SMul α β] [IsScalarTower G α β] (a : α) (b : simpa only [mem_stabilizer_iff, ← smul_assoc, h.eq_iff] using ha @[to_additive (attr := simp)] -lemma stabilizer_smul_eq_right [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) : +lemma stabilizer_smul_eq_right {α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) : stabilizer G (a • b) = stabilizer G b := (le_stabilizer_smul_right _ _).antisymm' <| (le_stabilizer_smul_right a⁻¹ _).trans_eq <| by rw [inv_smul_smul] diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index 5b525acc8b901..1d055b96f86dc 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -119,8 +119,8 @@ theorem _root_.MulActionHom.toQuotient_apply (H : Subgroup α) (g : α) : instance mulLeftCosetsCompSubtypeVal (H I : Subgroup α) : MulAction I (α ⧸ H) := MulAction.compHom (α ⧸ H) (Subgroup.subtype I) --- Porting note: Needed to insert [Group α] here -variable (α) [Group α] [MulAction α β] (x : β) +variable (α) +variable [MulAction α β] (x : β) /-- The canonical map from the quotient of the stabilizer to the set. -/ @[to_additive "The canonical map from the quotient of the stabilizer to the set. "] diff --git a/Mathlib/GroupTheory/NoncommPiCoprod.lean b/Mathlib/GroupTheory/NoncommPiCoprod.lean index 46cb605a70f01..52503c3b5a08c 100644 --- a/Mathlib/GroupTheory/NoncommPiCoprod.lean +++ b/Mathlib/GroupTheory/NoncommPiCoprod.lean @@ -81,7 +81,7 @@ variable {M : Type*} [Monoid M] -- We have a family of monoids -- The fintype assumption is not always used, but declared here, to keep things in order -variable {ι : Type*} [DecidableEq ι] [Fintype ι] +variable {ι : Type*} [Fintype ι] variable {N : ι → Type*} [∀ i, Monoid (N i)] -- And morphisms ϕ into G @@ -114,7 +114,7 @@ def noncommPiCoprod : (∀ i : ι, N i) →* M where variable {hcomm} @[to_additive (attr := simp)] -theorem noncommPiCoprod_mulSingle (i : ι) (y : N i) : +theorem noncommPiCoprod_mulSingle [DecidableEq ι] (i : ι) (y : N i) : noncommPiCoprod ϕ hcomm (Pi.mulSingle i y) = ϕ i y := by change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _) = ϕ i y @@ -130,7 +130,7 @@ theorem noncommPiCoprod_mulSingle (i : ι) (y : N i) : /-- The universal property of `MonoidHom.noncommPiCoprod` -/ @[to_additive "The universal property of `AddMonoidHom.noncommPiCoprod`"] -def noncommPiCoprodEquiv : +def noncommPiCoprodEquiv [DecidableEq ι] : { ϕ : ∀ i, N i →* M // Pairwise fun i j => ∀ x y, Commute (ϕ i x) (ϕ j y) } ≃ ((∀ i, N i) →* M) where toFun ϕ := noncommPiCoprod ϕ.1 ϕ.2 @@ -164,7 +164,7 @@ end FamilyOfMonoids section FamilyOfGroups variable {G : Type*} [Group G] -variable {ι : Type*} [hdec : DecidableEq ι] [hfin : Fintype ι] +variable {ι : Type*} variable {H : ι → Type*} [∀ i, Group (H i)] variable (ϕ : ∀ i : ι, H i →* G) @@ -174,7 +174,7 @@ variable (f g : ∀ i : ι, H i) namespace MonoidHom -- The subgroup version of `MonoidHom.noncommPiCoprod_mrange` @[to_additive] -theorem noncommPiCoprod_range +theorem noncommPiCoprod_range [Fintype ι] {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} : (noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range := by letI := Classical.decEq ι @@ -190,7 +190,7 @@ theorem noncommPiCoprod_range exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩ @[to_additive] -theorem injective_noncommPiCoprod_of_independent +theorem injective_noncommPiCoprod_of_independent [Fintype ι] {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} (hind : CompleteLattice.Independent fun i => (ϕ i).range) (hinj : ∀ i, Function.Injective (ϕ i)) : Function.Injective (noncommPiCoprod ϕ hcomm) := by @@ -249,7 +249,7 @@ namespace Subgroup -- We have a family of subgroups variable {G : Type*} [Group G] -variable {ι : Type*} [hdec : DecidableEq ι] [hfin : Fintype ι] {H : ι → Subgroup G} +variable {ι : Type*} {H : ι → Subgroup G} -- Elements of `Π (i : ι), H i` are called `f` and `g` here variable (f g : ∀ i : ι, H i) @@ -267,6 +267,18 @@ theorem commute_subtype_of_commute rintro ⟨x, hx⟩ ⟨y, hy⟩ exact hcomm hne x y hx hy +@[to_additive] +theorem independent_of_coprime_order + (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) + [Finite ι] [∀ i, Fintype (H i)] + (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : + CompleteLattice.Independent H := by + simpa using + MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype) + (commute_subtype_of_commute hcomm) hcoprime + +variable [Fintype ι] + /-- The canonical homomorphism from a family of subgroups where elements from different subgroups commute -/ @[to_additive "The canonical homomorphism from a family of additive subgroups where elements from @@ -276,7 +288,7 @@ def noncommPiCoprod (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → MonoidHom.noncommPiCoprod (fun i => (H i).subtype) (commute_subtype_of_commute hcomm) @[to_additive (attr := simp)] -theorem noncommPiCoprod_mulSingle +theorem noncommPiCoprod_mulSingle [DecidableEq ι] {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}(i : ι) (y : H i) : noncommPiCoprod hcomm (Pi.mulSingle i y) = y := by apply MonoidHom.noncommPiCoprod_mulSingle @@ -296,16 +308,6 @@ theorem injective_noncommPiCoprod_of_independent · intro i exact Subtype.coe_injective -@[to_additive] -theorem independent_of_coprime_order - (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) - [Finite ι] [∀ i, Fintype (H i)] - (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) : - CompleteLattice.Independent H := by - simpa using - MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype) - (commute_subtype_of_commute hcomm) hcoprime - end CommutingSubgroups end Subgroup diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index 9e37e57b20ea2..faa4010f0d09f 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -751,10 +751,28 @@ lemma orderOf_eq_card_powers : orderOf x = Fintype.card (powers x : Set G) := end FiniteCancelMonoid section FiniteGroup -variable [Group G] +variable [Group G] {x y : G} + +@[to_additive] +theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by + rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one] + + +@[to_additive] +theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by + rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd, + zero_sub, neg_sub] + +@[to_additive (attr := simp)] +theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x := by + refine ⟨?_, fun h n m hnm => ?_⟩ + · simp_rw [isOfFinOrder_iff_pow_eq_one] + rintro h ⟨n, hn, hx⟩ + exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx) + rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm section Finite -variable [Finite G] {x y : G} +variable [Finite G] @[to_additive] theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1 := by @@ -776,23 +794,6 @@ lemma mem_zpowers_iff_mem_range_orderOf [DecidableEq G] : y ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) := (isOfFinOrder_of_finite _).mem_zpowers_iff_mem_range_orderOf -@[to_additive] -theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by - rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one] - -@[to_additive] -theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by - rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd, - zero_sub, neg_sub] - -@[to_additive (attr := simp)] -theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x := by - refine ⟨?_, fun h n m hnm => ?_⟩ - · simp_rw [isOfFinOrder_iff_pow_eq_one] - rintro h ⟨n, hn, hx⟩ - exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx) - rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm - /-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping `x ^ i` to `y ^ i`. -/ @[to_additive @@ -862,18 +863,18 @@ theorem orderOf_dvd_natCard {G : Type*} [Group G] (x : G) : orderOf x ∣ Nat.ca · simp only [card_eq_zero_of_infinite, dvd_zero] @[to_additive] -nonrec lemma Subgroup.orderOf_dvd_natCard (s : Subgroup G) (hx : x ∈ s) : +nonrec lemma Subgroup.orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G) {x} (hx : x ∈ s) : orderOf x ∣ Nat.card s := by simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s) @[to_additive] -lemma Subgroup.orderOf_le_card (s : Subgroup G) (hs : (s : Set G).Finite) (hx : x ∈ s) : - orderOf x ≤ Nat.card s := +lemma Subgroup.orderOf_le_card {G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite) + {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s := le_of_dvd (Nat.card_pos_iff.2 <| ⟨s.coe_nonempty.to_subtype, hs.to_subtype⟩) <| s.orderOf_dvd_natCard hx @[to_additive] -lemma Submonoid.orderOf_le_card (s : Submonoid G) (hs : (s : Set G).Finite) (hx : x ∈ s) : - orderOf x ≤ Nat.card s := by +lemma Submonoid.orderOf_le_card {G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite) + {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s := by rw [← Nat.card_submonoidPowers]; exact Nat.card_mono hs <| powers_le.2 hx @[to_additive (attr := simp) card_nsmul_eq_zero'] @@ -899,11 +900,11 @@ theorem zpow_mod_card (a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf] @[to_additive (attr := simp) mod_natCard_nsmul] -lemma pow_mod_natCard (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by +lemma pow_mod_natCard {G} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n $ orderOf_dvd_natCard _, pow_mod_orderOf] @[to_additive (attr := simp) mod_natCard_zsmul] -lemma zpow_mod_natCard (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by +lemma zpow_mod_natCard {G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n $ Int.natCast_dvd_natCast.2 $ orderOf_dvd_natCard _, zpow_mod_orderOf] @@ -933,7 +934,8 @@ theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).Coprime n) {g : G inv_pow g n @[to_additive Nat.Coprime.nsmul_right_bijective] -lemma Nat.Coprime.pow_left_bijective (hn : (Nat.card G).Coprime n) : Bijective (· ^ n : G → G) := +lemma Nat.Coprime.pow_left_bijective {G} [Group G] (hn : (Nat.card G).Coprime n) : + Bijective (· ^ n : G → G) := (powCoprime hn).bijective @[to_additive add_inf_eq_bot_of_coprime] @@ -1080,11 +1082,13 @@ lemma Nat.cast_card_eq_zero (R) [AddGroupWithOne R] [Fintype R] : (Fintype.card rw [← nsmul_one, card_nsmul_eq_zero] section NonAssocRing -variable (R : Type*) [NonAssocRing R] [Fintype R] (p : ℕ) +variable (R : Type*) [NonAssocRing R] (p : ℕ) lemma CharP.addOrderOf_one : CharP R (addOrderOf (1 : R)) where cast_eq_zero_iff' n := by rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero] +variable [Fintype R] + variable {R} in lemma charP_of_ne_zero (hn : card R = p) (hR : ∀ i < p, (i : R) = 0 → i = 0) : CharP R p where cast_eq_zero_iff' n := by diff --git a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean index 99e9da84fbd04..06e8e9cdedfb5 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean @@ -36,7 +36,7 @@ namespace Equiv.Perm section CycleOf -variable {f g : Perm α} {x y : α} [DecidableRel f.SameCycle] [DecidableRel g.SameCycle] +variable {f g : Perm α} {x y : α} /-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/ def cycleOf (f : Perm α) [DecidableRel f.SameCycle] (x : α) : Perm α := @@ -74,13 +74,16 @@ theorem cycleOf_zpow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α · exact cycleOf_pow_apply_self f x z · rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self] -theorem SameCycle.cycleOf_apply : SameCycle f x y → cycleOf f x y = f y := +theorem SameCycle.cycleOf_apply [DecidableRel f.SameCycle] : + SameCycle f x y → cycleOf f x y = f y := ofSubtype_apply_of_mem _ -theorem cycleOf_apply_of_not_sameCycle : ¬SameCycle f x y → cycleOf f x y = y := +theorem cycleOf_apply_of_not_sameCycle [DecidableRel f.SameCycle] : + ¬SameCycle f x y → cycleOf f x y = y := ofSubtype_apply_of_not_mem _ -theorem SameCycle.cycleOf_eq (h : SameCycle f x y) : cycleOf f x = cycleOf f y := by +theorem SameCycle.cycleOf_eq [DecidableRel f.SameCycle] (h : SameCycle f x y) : + cycleOf f x = cycleOf f y := by ext z rw [Equiv.Perm.cycleOf_apply] split_ifs with hz @@ -108,7 +111,8 @@ theorem cycleOf_apply_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : theorem cycleOf_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) : cycleOf f x x = f x := SameCycle.rfl.cycleOf_apply -theorem IsCycle.cycleOf_eq (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f := +theorem IsCycle.cycleOf_eq [DecidableRel f.SameCycle] + (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f := Equiv.ext fun y => if h : SameCycle f x y then by rw [h.cycleOf_apply] else by @@ -138,8 +142,8 @@ theorem cycleOf_self_apply_zpow (f : Perm α) [DecidableRel f.SameCycle] (n : cycleOf f ((f ^ n) x) = cycleOf f x := SameCycle.rfl.zpow_left.cycleOf_eq -protected theorem IsCycle.cycleOf [DecidableEq α] (hf : IsCycle f) : - cycleOf f x = if f x = x then 1 else f := by +protected theorem IsCycle.cycleOf [DecidableRel f.SameCycle] [DecidableEq α] + (hf : IsCycle f) : cycleOf f x = if f x = x then 1 else f := by by_cases hx : f x = x · rwa [if_pos hx, cycleOf_eq_one_iff] · rwa [if_neg hx, hf.cycleOf_eq] @@ -181,7 +185,8 @@ theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] ( (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf] -theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel (f * g).SameCycle] +theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel f.SameCycle] + [DecidableRel (f * g).SameCycle] (h : Commute f g) (x : α) (hx : g x = x) : (f * g).cycleOf x = f.cycleOf x := by ext y by_cases hxy : (f * g).SameCycle x y @@ -194,8 +199,8 @@ theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel (f * g).SameCycle] refine ⟨z, ?_⟩ simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx] -theorem Disjoint.cycleOf_mul_distrib [DecidableRel (f * g).SameCycle] - [DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) : +theorem Disjoint.cycleOf_mul_distrib [DecidableRel f.SameCycle] [DecidableRel g.SameCycle] + [DecidableRel (f * g).SameCycle] [DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) : (f * g).cycleOf x = f.cycleOf x * g.cycleOf x := by cases' (disjoint_iff_eq_or_eq.mp h) x with hfx hgx · simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx] diff --git a/Mathlib/GroupTheory/PresentedGroup.lean b/Mathlib/GroupTheory/PresentedGroup.lean index 42f21ec785c7d..184b89f21a66b 100644 --- a/Mathlib/GroupTheory/PresentedGroup.lean +++ b/Mathlib/GroupTheory/PresentedGroup.lean @@ -64,25 +64,24 @@ variable {G : Type*} [Group G] {f : α → G} {rels : Set (FreeGroup α)} local notation "F" => FreeGroup.lift f --- Porting note: `F` has been expanded, because `F r = 1` produces a sorry. -variable (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) - -theorem closure_rels_subset_ker : Subgroup.normalClosure rels ≤ MonoidHom.ker F := +theorem closure_rels_subset_ker (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) : + Subgroup.normalClosure rels ≤ MonoidHom.ker F := Subgroup.normalClosure_le_normal fun x w ↦ (MonoidHom.mem_ker _).2 (h x w) -theorem to_group_eq_one_of_mem_closure : ∀ x ∈ Subgroup.normalClosure rels, F x = 1 := +theorem to_group_eq_one_of_mem_closure (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) : + ∀ x ∈ Subgroup.normalClosure rels, F x = 1 := fun _ w ↦ (MonoidHom.mem_ker _).1 <| closure_rels_subset_ker h w /-- The extension of a map `f : α → G` that satisfies the given relations to a group homomorphism from `PresentedGroup rels → G`. -/ -def toGroup : PresentedGroup rels →* G := +def toGroup (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) : PresentedGroup rels →* G := QuotientGroup.lift (Subgroup.normalClosure rels) F (to_group_eq_one_of_mem_closure h) @[simp] -theorem toGroup.of {x : α} : toGroup h (of x) = f x := +theorem toGroup.of (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) {x : α} : toGroup h (of x) = f x := FreeGroup.lift.of -theorem toGroup.unique (g : PresentedGroup rels →* G) +theorem toGroup.unique (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) (g : PresentedGroup rels →* G) (hg : ∀ x : α, g (PresentedGroup.of x) = f x) : ∀ {x}, g x = toGroup h x := by intro x refine QuotientGroup.induction_on x ?_ diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean index dcbb87fc05ba1..5cfcdcf416e0e 100644 --- a/Mathlib/SetTheory/Cardinal/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean @@ -758,9 +758,10 @@ variable {ι : Type u} {ι' : Type w} (f : ι → Cardinal.{v}) section add -variable [Nonempty ι] [Nonempty ι'] (hf : BddAbove (range f)) +variable [Nonempty ι] [Nonempty ι'] -protected theorem ciSup_add (c : Cardinal.{v}) : (⨆ i, f i) + c = ⨆ i, f i + c := by +protected theorem ciSup_add (hf : BddAbove (range f)) (c : Cardinal.{v}) : + (⨆ i, f i) + c = ⨆ i, f i + c := by have : ∀ i, f i + c ≤ (⨆ i, f i) + c := fun i ↦ add_le_add_right (le_ciSup hf i) c refine le_antisymm ?_ (ciSup_le' this) have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩ @@ -772,10 +773,12 @@ protected theorem ciSup_add (c : Cardinal.{v}) : (⨆ i, f i) + c = ⨆ i, f i + exact ⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c, (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩ -protected theorem add_ciSup (c : Cardinal.{v}) : c + (⨆ i, f i) = ⨆ i, c + f i := by +protected theorem add_ciSup (hf : BddAbove (range f)) (c : Cardinal.{v}) : + c + (⨆ i, f i) = ⨆ i, c + f i := by rw [add_comm, Cardinal.ciSup_add f hf]; simp_rw [add_comm] -protected theorem ciSup_add_ciSup (g : ι' → Cardinal.{v}) (hg : BddAbove (range g)) : +protected theorem ciSup_add_ciSup (hf : BddAbove (range f)) (g : ι' → Cardinal.{v}) + (hg : BddAbove (range g)) : (⨆ i, f i) + (⨆ j, g j) = ⨆ (i) (j), f i + g j := by simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg] diff --git a/Mathlib/SetTheory/Surreal/Multiplication.lean b/Mathlib/SetTheory/Surreal/Multiplication.lean index d89da018a18f7..362a8f555a1af 100644 --- a/Mathlib/SetTheory/Surreal/Multiplication.lean +++ b/Mathlib/SetTheory/Surreal/Multiplication.lean @@ -453,26 +453,30 @@ namespace SetTheory.PGame open Surreal.Multiplication variable {x x₁ x₂ y y₁ y₂ : PGame.{u}} - (hx : x.Numeric) (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) - (hy : y.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) -theorem Numeric.mul : Numeric (x * y) := main _ <| Args.numeric_P1.mpr ⟨hx, hy⟩ +theorem Numeric.mul (hx : x.Numeric) (hy : y.Numeric) : Numeric (x * y) := + main _ <| Args.numeric_P1.mpr ⟨hx, hy⟩ -theorem P24 : P24 x₁ x₂ y := main _ <| Args.numeric_P24.mpr ⟨hx₁, hx₂, hy⟩ +theorem P24 (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) : P24 x₁ x₂ y := + main _ <| Args.numeric_P24.mpr ⟨hx₁, hx₂, hy⟩ -theorem Equiv.mul_congr_left (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y := +theorem Equiv.mul_congr_left (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy : y.Numeric) + (he : x₁ ≈ x₂) : x₁ * y ≈ x₂ * y := equiv_iff_game_eq.2 <| (P24 hx₁ hx₂ hy).1 he -theorem Equiv.mul_congr_right (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂ := +theorem Equiv.mul_congr_right (hx : x.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) + (he : y₁ ≈ y₂) : x * y₁ ≈ x * y₂ := .trans (mul_comm_equiv _ _) <| .trans (mul_congr_left hy₁ hy₂ hx he) (mul_comm_equiv _ _) -theorem Equiv.mul_congr (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂ := +theorem Equiv.mul_congr (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) + (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ * y₁ ≈ x₂ * y₂ := .trans (mul_congr_left hx₁ hx₂ hy₁ hx) (mul_congr_right hx₂ hy₁ hy₂ hy) open Prod.GameAdd /-- One additional inductive argument that supplies the last missing part of Theorem 8. -/ -theorem P3_of_lt_of_lt (hx : x₁ < x₂) (hy : y₁ < y₂) : P3 x₁ x₂ y₁ y₂ := by +theorem P3_of_lt_of_lt (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) + (hx : x₁ < x₂) (hy : y₁ < y₂) : P3 x₁ x₂ y₁ y₂ := by revert x₁ x₂ rw [← Prod.forall'] refine (wf_isOption.prod_gameAdd wf_isOption).fix ?_ @@ -488,7 +492,8 @@ theorem P3_of_lt_of_lt (hx : x₁ < x₂) (hy : y₁ < y₂) : P3 x₁ x₂ y₁ rw [moveLeft_neg', ← P3_neg, neg_lt_neg_iff] exact ih _ (fst <| IsOption.moveRight _) (hx₁.moveRight _) hx₂⟩ -theorem Numeric.mul_pos (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) : 0 < x₁ * x₂ := by +theorem Numeric.mul_pos (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hp₁ : 0 < x₁) (hp₂ : 0 < x₂) : + 0 < x₁ * x₂ := by rw [lt_iff_game_lt] have := P3_of_lt_of_lt numeric_zero hx₁ numeric_zero hx₂ hp₁ hp₂ simp_rw [P3, quot_zero_mul, quot_mul_zero, add_lt_add_iff_left] at this diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 104d1001f6c2e..7930817c3788d 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -242,7 +242,7 @@ protected theorem IsTopologicalBasis.inducing {β} [TopologicalSpace β] {f : α convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s aesop -protected theorem IsTopologicalBasis.induced [s : TopologicalSpace β] (f : α → β) +protected theorem IsTopologicalBasis.induced {α} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)} (h : IsTopologicalBasis T) : IsTopologicalBasis (t := induced f s) ((preimage f) '' T) := h.inducing (t := induced f s) (inducing_induced f) @@ -711,7 +711,7 @@ protected theorem IsTopologicalBasis.secondCountableTopology {b : Set (Set α)} (hb : IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α := ⟨⟨b, hc, hb.eq_generateFrom⟩⟩ -lemma SecondCountableTopology.mk' {b : Set (Set α)} (hc : b.Countable) : +lemma SecondCountableTopology.mk' {α} {b : Set (Set α)} (hc : b.Countable) : @SecondCountableTopology α (generateFrom b) := @SecondCountableTopology.mk α (generateFrom b) ⟨b, hc, rfl⟩ @@ -769,7 +769,7 @@ instance (priority := 100) SecondCountableTopology.to_firstCountableTopology /-- If `β` is a second-countable space, then its induced topology via `f` on `α` is also second-countable. -/ -theorem secondCountableTopology_induced (β) [t : TopologicalSpace β] [SecondCountableTopology β] +theorem secondCountableTopology_induced (α β) [t : TopologicalSpace β] [SecondCountableTopology β] (f : α → β) : @SecondCountableTopology α (t.induced f) := by rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩ letI := t.induced f @@ -782,7 +782,7 @@ instance Subtype.secondCountableTopology (s : Set α) [SecondCountableTopology SecondCountableTopology s := secondCountableTopology_induced s α (↑) -lemma secondCountableTopology_iInf {ι} [Countable ι] {t : ι → TopologicalSpace α} +lemma secondCountableTopology_iInf {α ι} [Countable ι] {t : ι → TopologicalSpace α} (ht : ∀ i, @SecondCountableTopology α (t i)) : @SecondCountableTopology α (⨅ i, t i) := by rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion] exact SecondCountableTopology.mk' <| @@ -884,7 +884,7 @@ end Sigma section Sum -variable {β : Type*} [TopologicalSpace α] [TopologicalSpace β] +variable {β : Type*} [TopologicalSpace β] /-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of topological bases on each of the two components. -/ @@ -964,18 +964,19 @@ end TopologicalSpace open TopologicalSpace -variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} +variable {α β : Type*} [TopologicalSpace α] {f : α → β} -protected theorem Inducing.secondCountableTopology [SecondCountableTopology β] (hf : Inducing f) : - SecondCountableTopology α := by +protected theorem Inducing.secondCountableTopology [TopologicalSpace β] [SecondCountableTopology β] + (hf : Inducing f) : SecondCountableTopology α := by rw [hf.1] exact secondCountableTopology_induced α β f -protected theorem Embedding.secondCountableTopology [SecondCountableTopology β] (hf : Embedding f) : - SecondCountableTopology α := +protected theorem Embedding.secondCountableTopology + [TopologicalSpace β] [SecondCountableTopology β] + (hf : Embedding f) : SecondCountableTopology α := hf.1.secondCountableTopology -protected theorem Embedding.separableSpace [TopologicalSpace α] +protected theorem Embedding.separableSpace [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : Embedding f) : TopologicalSpace.SeparableSpace α := by have := hf.secondCountableTopology diff --git a/Mathlib/Topology/Clopen.lean b/Mathlib/Topology/Clopen.lean index 64561f2afd57f..2a18e7931ec4e 100644 --- a/Mathlib/Topology/Clopen.lean +++ b/Mathlib/Topology/Clopen.lean @@ -59,27 +59,27 @@ lemma IsClopen.himp (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t) := theorem IsClopen.prod {t : Set Y} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ×ˢ t) := ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩ -theorem isClopen_iUnion_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : +theorem isClopen_iUnion_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋃ i, s i) := ⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩ -theorem Set.Finite.isClopen_biUnion {s : Set Y} {f : Y → Set X} (hs : s.Finite) +theorem Set.Finite.isClopen_biUnion {Y} {s : Set Y} {f : Y → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) := ⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩ -theorem isClopen_biUnion_finset {s : Finset Y} {f : Y → Set X} +theorem isClopen_biUnion_finset {Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) := s.finite_toSet.isClopen_biUnion h -theorem isClopen_iInter_of_finite [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : +theorem isClopen_iInter_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋂ i, s i) := ⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩ -theorem Set.Finite.isClopen_biInter {s : Set Y} (hs : s.Finite) {f : Y → Set X} +theorem Set.Finite.isClopen_biInter {Y} {s : Set Y} (hs : s.Finite) {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) := ⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩ -theorem isClopen_biInter_finset {s : Finset Y} {f : Y → Set X} +theorem isClopen_biInter_finset {Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) := s.finite_toSet.isClopen_biInter h diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 25d4221e631a8..3cdc5fe127909 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -51,6 +51,7 @@ Mathlib/Order/LiminfLimsup.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1791 Mathlib/Order/UpperLower/Basic.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1795 lines, try to split it up Mathlib/RingTheory/UniqueFactorizationDomain.lean : line 1 : ERR_NUM_LIN : 2100 file contains 1982 lines, try to split it up Mathlib/SetTheory/Cardinal/Basic.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2004 lines, try to split it up +Mathlib/SetTheory/Cardinal/Ordinal.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1501 lines, try to split it up Mathlib/SetTheory/Game/PGame.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1753 lines, try to split it up Mathlib/SetTheory/Ordinal/Arithmetic.lean : line 1 : ERR_NUM_LIN : 2400 file contains 2269 lines, try to split it up Mathlib/SetTheory/ZFC/Basic.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1549 lines, try to split it up