Skip to content

Commit b1dfc8c

Browse files
mattrobballmattrobball
committed
fix some files
1 parent 0c9345f commit b1dfc8c

123 files changed

Lines changed: 230 additions & 231 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Mathlib/Algebra/Algebra/Hom.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B where
112112
#align alg_hom.alg_hom_class AlgHom.algHomClass
113113

114114
/-- See Note [custom simps projection] -/
115-
def Simps.apply {R α β : Type*} [CommSemiring R]
115+
def Simps.apply {R α β : Type _} [CommSemiring R]
116116
[Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) : α → β := f
117117

118118
initialize_simps_projections AlgHom (toFun → apply)

‎Mathlib/Algebra/Algebra/RestrictScalars.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ Note that this means we almost always want to state definitions and lemmas in th
7575
An example of when one might want to use `RestrictScalars` would be if one has a vector space
7676
over a field of characteristic zero and wishes to make use of the `ℚ`-algebra structure. -/
7777
@[nolint unusedArguments]
78-
def RestrictScalars (_R _S M : Type*) : Type* := M
78+
def RestrictScalars (_R _S M : Type*) : Type _ := M
7979
#align restrict_scalars RestrictScalars
8080

8181
instance [I : Inhabited M] : Inhabited (RestrictScalars R S M) := I

‎Mathlib/Algebra/Algebra/Subalgebra/Basic.lean‎

Lines changed: 27 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ variable (S : Subalgebra R A)
104104
instance instSMulMemClass : SMulMemClass (Subalgebra R A) R A where
105105
smul_mem {S} r x hx := (Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem' r) hx
106106

107-
theorem _root_.algebraMap_mem {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
107+
theorem _root_.algebraMap_mem {S R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
108108
[SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) :
109109
algebraMap R A r ∈ s :=
110110
Algebra.algebraMap_eq_smul_one (A := A) r ▸ SMulMemClass.smul_mem r (one_mem s)
@@ -184,7 +184,7 @@ protected theorem prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemir
184184
prod_mem h
185185
#align subalgebra.prod_mem Subalgebra.prod_mem
186186

187-
instance {R A : Type*} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
187+
instance {R A : Type _} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A :=
188188
{ Subalgebra.SubsemiringClass with
189189
neg_mem := fun {S x} hx => neg_one_smul R x ▸ S.smul_mem hx _ }
190190

@@ -454,7 +454,7 @@ theorem toSubsemiring_subtype : S.toSubsemiring.subtype = (S.val : S →+* A) :=
454454
#align subalgebra.to_subsemiring_subtype Subalgebra.toSubsemiring_subtype
455455

456456
@[simp]
457-
theorem toSubring_subtype {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
457+
theorem toSubring_subtype {R A : Type _} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) :
458458
S.toSubring.subtype = (S.val : S →+* A) := rfl
459459
#align subalgebra.to_subring_subtype Subalgebra.toSubring_subtype
460460

@@ -532,12 +532,12 @@ theorem coe_comap (S : Subalgebra R B) (f : A →ₐ[R] B) : (S.comap f : Set A)
532532
rfl
533533
#align subalgebra.coe_comap Subalgebra.coe_comap
534534

535-
instance noZeroDivisors {R A : Type*} [CommSemiring R] [Semiring A] [NoZeroDivisors A]
535+
instance noZeroDivisors {R A : Type _} [CommSemiring R] [Semiring A] [NoZeroDivisors A]
536536
[Algebra R A] (S : Subalgebra R A) : NoZeroDivisors S :=
537537
inferInstanceAs (NoZeroDivisors S.toSubsemiring)
538538
#align subalgebra.no_zero_divisors Subalgebra.noZeroDivisors
539539

540-
instance isDomain {R A : Type*} [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
540+
instance isDomain {R A : Type _} [CommRing R] [Ring A] [IsDomain A] [Algebra R A]
541541
(S : Subalgebra R A) : IsDomain S :=
542542
inferInstanceAs (IsDomain S.toSubring)
543543
#align subalgebra.is_domain Subalgebra.isDomain
@@ -546,7 +546,7 @@ end Subalgebra
546546

547547
namespace Submodule
548548

549-
variable {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
549+
variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A]
550550

551551
variable (p : Submodule R A)
552552

@@ -733,7 +733,7 @@ theorem ofInjective_apply (f : A →ₐ[R] B) (hf : Function.Injective f) (x : A
733733
#align alg_equiv.of_injective_apply AlgEquiv.ofInjective_apply
734734

735735
/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/
736-
noncomputable def ofInjectiveField {E F : Type*} [DivisionRing E] [Semiring F] [Nontrivial F]
736+
noncomputable def ofInjectiveField {E F : Type _} [DivisionRing E] [Semiring F] [Nontrivial F]
737737
[Algebra R E] [Algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range :=
738738
ofInjective f f.toRingHom.injective
739739
#align alg_equiv.of_injective_field AlgEquiv.ofInjectiveField
@@ -798,7 +798,7 @@ theorem top_toSubsemiring : (⊤ : Subalgebra R A).toSubsemiring = ⊤ := rfl
798798
#align algebra.top_to_subsemiring Algebra.top_toSubsemiring
799799

800800
@[simp]
801-
theorem top_toSubring {R A : Type*} [CommRing R] [Ring A] [Algebra R A] :
801+
theorem top_toSubring {R A : Type _} [CommRing R] [Ring A] [Algebra R A] :
802802
(⊤ : Subalgebra R A).toSubring = ⊤ := rfl
803803
#align algebra.top_to_subring Algebra.top_toSubring
804804

@@ -813,7 +813,7 @@ theorem toSubsemiring_eq_top {S : Subalgebra R A} : S.toSubsemiring = ⊤ ↔ S
813813
#align algebra.to_subsemiring_eq_top Algebra.toSubsemiring_eq_top
814814

815815
@[simp]
816-
theorem toSubring_eq_top {R A : Type*} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :
816+
theorem toSubring_eq_top {R A : Type _} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :
817817
S.toSubring = ⊤ ↔ S = ⊤ :=
818818
Subalgebra.toSubring_injective.eq_iff' top_toSubring
819819
#align algebra.to_subring_eq_top Algebra.toSubring_eq_top
@@ -955,7 +955,7 @@ theorem surjective_algebraMap_iff :
955955
fun h y => Algebra.mem_bot.1 <| eq_bot_iff.1 h (Algebra.mem_top : y ∈ _)⟩
956956
#align algebra.surjective_algebra_map_iff Algebra.surjective_algebraMap_iff
957957

958-
theorem bijective_algebraMap_iff {R A : Type*} [Field R] [Semiring A] [Nontrivial A]
958+
theorem bijective_algebraMap_iff {R A : Type _} [Field R] [Semiring A] [Nontrivial A]
959959
[Algebra R A] : Function.Bijective (algebraMap R A) ↔ (⊤ : Subalgebra R A) = ⊥ :=
960960
⟨fun h => surjective_algebraMap_iff.1 h.2, fun h =>
961961
⟨(algebraMap R A).injective, surjective_algebraMap_iff.2 h⟩⟩
@@ -973,7 +973,7 @@ noncomputable def botEquivOfInjective (h : Function.Injective (algebraMap R A))
973973

974974
/-- The bottom subalgebra is isomorphic to the field. -/
975975
@[simps! symm_apply]
976-
noncomputable def botEquiv (F R : Type*) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
976+
noncomputable def botEquiv (F R : Type _) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
977977
(⊥ : Subalgebra F R) ≃ₐ[F] F :=
978978
botEquivOfInjective (RingHom.injective _)
979979
#align algebra.bot_equiv Algebra.botEquiv
@@ -1146,7 +1146,7 @@ end Prod
11461146

11471147
section SuprLift
11481148

1149-
variable {ι : Type*}
1149+
variable {ι : Type _}
11501150

11511151
theorem coe_iSup_of_directed [Nonempty ι] {S : ι → Subalgebra R A} (dir : Directed (· ≤ ·) S) :
11521152
↑(iSup S) = ⋃ i, (S i : Set A) :=
@@ -1246,7 +1246,7 @@ These are just copies of the definitions about `Subsemiring` starting from
12461246

12471247
section Actions
12481248

1249-
variable {α β : Type*}
1249+
variable {α β : Type _}
12501250

12511251
/-- The action by a subalgebra is the action by the underlying algebra. -/
12521252
instance [SMul A α] (S : Subalgebra R A) : SMul S α :=
@@ -1271,7 +1271,7 @@ instance isScalarTower_left [SMul α β] [SMul A α] [SMul A β] [IsScalarTower
12711271
inferInstanceAs (IsScalarTower S.toSubsemiring α β)
12721272
#align subalgebra.is_scalar_tower_left Subalgebra.isScalarTower_left
12731273

1274-
instance isScalarTower_mid {R S T : Type*} [CommSemiring R] [Semiring S] [AddCommMonoid T]
1274+
instance isScalarTower_mid {R S T : Type _} [CommSemiring R] [Semiring S] [AddCommMonoid T]
12751275
[Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) :
12761276
IsScalarTower R S' T :=
12771277
⟨fun _x y _z => (smul_assoc _ (y : S) _ : _)⟩
@@ -1302,25 +1302,25 @@ instance moduleLeft [AddCommMonoid α] [Module A α] (S : Subalgebra R A) : Modu
13021302
#align subalgebra.module_left Subalgebra.moduleLeft
13031303

13041304
/-- The action by a subalgebra is the action by the underlying algebra. -/
1305-
instance toAlgebra {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
1305+
instance toAlgebra {R A : Type _} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
13061306
[Algebra A α] (S : Subalgebra R A) : Algebra S α :=
13071307
Algebra.ofSubsemiring S.toSubsemiring
13081308
#align subalgebra.to_algebra Subalgebra.toAlgebra
13091309

1310-
theorem algebraMap_eq {R A : Type*} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
1310+
theorem algebraMap_eq {R A : Type _} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A]
13111311
[Algebra A α] (S : Subalgebra R A) : algebraMap S α = (algebraMap A α).comp S.val :=
13121312
rfl
13131313
#align subalgebra.algebra_map_eq Subalgebra.algebraMap_eq
13141314

13151315
@[simp]
1316-
theorem rangeS_algebraMap {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
1316+
theorem rangeS_algebraMap {R A : Type _} [CommSemiring R] [CommSemiring A] [Algebra R A]
13171317
(S : Subalgebra R A) : (algebraMap S A).rangeS = S.toSubsemiring := by
13181318
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubsemiring_subtype,
13191319
Subsemiring.rangeS_subtype]
13201320
#align subalgebra.srange_algebra_map Subalgebra.rangeS_algebraMap
13211321

13221322
@[simp]
1323-
theorem range_algebraMap {R A : Type*} [CommRing R] [CommRing A] [Algebra R A]
1323+
theorem range_algebraMap {R A : Type _} [CommRing R] [CommRing A] [Algebra R A]
13241324
(S : Subalgebra R A) : (algebraMap S A).range = S.toSubring := by
13251325
rw [algebraMap_eq, Algebra.id.map_eq_id, RingHom.id_comp, ← toSubring_subtype,
13261326
Subring.range_subtype]
@@ -1358,13 +1358,13 @@ theorem center_toSubsemiring : (center R A).toSubsemiring = Subsemiring.center A
13581358
#align subalgebra.center_to_subsemiring Subalgebra.center_toSubsemiring
13591359

13601360
@[simp]
1361-
theorem center_toSubring (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
1361+
theorem center_toSubring (R A : Type _) [CommRing R] [Ring A] [Algebra R A] :
13621362
(center R A).toSubring = Subring.center A :=
13631363
rfl
13641364
#align subalgebra.center_to_subring Subalgebra.center_toSubring
13651365

13661366
@[simp]
1367-
theorem center_eq_top (A : Type*) [CommSemiring A] [Algebra R A] : center R A = ⊤ :=
1367+
theorem center_eq_top (A : Type _) [CommSemiring A] [Algebra R A] : center R A = ⊤ :=
13681368
SetLike.coe_injective (Set.center_eq_univ A)
13691369
#align subalgebra.center_eq_top Subalgebra.center_eq_top
13701370

@@ -1373,7 +1373,7 @@ variable {R A}
13731373
instance : CommSemiring (center R A) :=
13741374
inferInstanceAs (CommSemiring (Subsemiring.center A))
13751375

1376-
instance {A : Type*} [Ring A] [Algebra R A] : CommRing (center R A) :=
1376+
instance {A : Type _} [Ring A] [Algebra R A] : CommRing (center R A) :=
13771377
inferInstanceAs (CommRing (Subring.center A))
13781378

13791379
theorem mem_center_iff {a : A} : a ∈ center R A ↔ ∀ b : A, b * a = a * b :=
@@ -1429,8 +1429,8 @@ end Centralizer
14291429
/-- Suppose we are given `∑ i, lᵢ * sᵢ = 1` in `S`, and `S'` a subalgebra of `S` that contains
14301430
`lᵢ` and `sᵢ`. To check that an `x : S` falls in `S'`, we only need to show that
14311431
`sᵢ ^ n • x ∈ S'` for some `n` for each `sᵢ`. -/
1432-
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type*} [CommRing S] [Algebra R S]
1433-
(S' : Subalgebra R S) {ι : Type*} (ι' : Finset ι) (s : ι → S) (l : ι → S)
1432+
theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Algebra R S]
1433+
(S' : Subalgebra R S) {ι : Type _} (ι' : Finset ι) (s : ι → S) (l : ι → S)
14341434
(e : ∑ i in ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
14351435
(H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
14361436
-- Porting note: needed to add this instance
@@ -1460,7 +1460,7 @@ theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type*} [CommRing S] [Algeb
14601460
exact ⟨⟨_, hn i⟩, rfl⟩
14611461
#align subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem
14621462

1463-
theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type*} [CommRing S] [Algebra R S]
1463+
theorem mem_of_span_eq_top_of_smul_pow_mem {S : Type _} [CommRing S] [Algebra R S]
14641464
(S' : Subalgebra R S) (s : Set S) (l : s →₀ S) (hs : Finsupp.total s S S (↑) l = 1)
14651465
(hs' : s ⊆ S') (hl : ∀ i, l i ∈ S') (x : S) (H : ∀ r : s, ∃ n : ℕ, (r : S) ^ n • x ∈ S') :
14661466
x ∈ S' :=
@@ -1471,7 +1471,7 @@ end Subalgebra
14711471

14721472
section Nat
14731473

1474-
variable {R : Type*} [Semiring R]
1474+
variable {R : Type _} [Semiring R]
14751475

14761476
/-- A subsemiring is an `ℕ`-subalgebra. -/
14771477
def subalgebraOfSubsemiring (S : Subsemiring R) : Subalgebra ℕ R :=
@@ -1488,7 +1488,7 @@ end Nat
14881488

14891489
section Int
14901490

1491-
variable {R : Type*} [Ring R]
1491+
variable {R : Type _} [Ring R]
14921492

14931493
/-- A subring is a `ℤ`-subalgebra. -/
14941494
def subalgebraOfSubring (S : Subring R) : Subalgebra ℤ R :=
@@ -1501,7 +1501,7 @@ def subalgebraOfSubring (S : Subring R) : Subalgebra ℤ R :=
15011501
exact S.sub_mem ih S.one_mem }
15021502
#align subalgebra_of_subring subalgebraOfSubring
15031503

1504-
variable {S : Type*} [Semiring S]
1504+
variable {S : Type _} [Semiring S]
15051505

15061506
@[simp]
15071507
theorem mem_subalgebraOfSubring {x : R} {S : Subring R} : x ∈ subalgebraOfSubring S ↔ x ∈ S :=

‎Mathlib/Algebra/Associated.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -727,7 +727,7 @@ end UniqueUnits₀
727727
/-- The quotient of a monoid by the `Associated` relation. Two elements `x` and `y`
728728
are associated iff there is a unit `u` such that `x * u = y`. There is a natural
729729
monoid structure on `Associates α`. -/
730-
abbrev Associates (α : Type*) [Monoid α] : Type* :=
730+
abbrev Associates (α : Type*) [Monoid α] : Type _ :=
731731
Quotient (Associated.setoid α)
732732
#align associates Associates
733733

‎Mathlib/Algebra/Category/GroupCat/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ set_option linter.uppercaseLean3 false in
144144
add_decl_doc AddGroupCat.ofHom
145145

146146
@[to_additive (attr := simp)]
147-
theorem ofHom_apply {X Y : Type*} [Group X] [Group Y] (f : X →* Y) (x : X) :
147+
theorem ofHom_apply {X Y : Type _} [Group X] [Group Y] (f : X →* Y) (x : X) :
148148
(ofHom f) x = f x :=
149149
rfl
150150
set_option linter.uppercaseLean3 false in
@@ -318,7 +318,7 @@ set_option linter.uppercaseLean3 false in
318318
add_decl_doc AddCommGroupCat.ofHom
319319

320320
@[to_additive (attr := simp)]
321-
theorem ofHom_apply {X Y : Type*} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :
321+
theorem ofHom_apply {X Y : Type _} [CommGroup X] [CommGroup Y] (f : X →* Y) (x : X) :
322322
(ofHom f) x = f x :=
323323
rfl
324324
set_option linter.uppercaseLean3 false in

‎Mathlib/Algebra/Category/Ring/Basic.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ set_option linter.uppercaseLean3 false in
103103
#align SemiRing.coe_of SemiRingCat.coe_of
104104

105105
@[simp]
106-
lemma RingEquiv_coe_eq {X Y : Type*} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
106+
lemma RingEquiv_coe_eq {X Y : Type _} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
107107
(@FunLike.coe (SemiRingCat.of X ⟶ SemiRingCat.of Y) _ (fun _ => (forget SemiRingCat).obj _)
108108
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
109109
rfl
@@ -242,7 +242,7 @@ set_option linter.uppercaseLean3 false in
242242
#align Ring.coe_of RingCat.coe_of
243243

244244
@[simp]
245-
lemma RingEquiv_coe_eq {X Y : Type*} [Ring X] [Ring Y] (e : X ≃+* Y) :
245+
lemma RingEquiv_coe_eq {X Y : Type _} [Ring X] [Ring Y] (e : X ≃+* Y) :
246246
(@FunLike.coe (RingCat.of X ⟶ RingCat.of Y) _ (fun _ => (forget RingCat).obj _)
247247
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
248248
rfl
@@ -325,7 +325,7 @@ set_option linter.uppercaseLean3 false in
325325
#align CommSemiRing.of_hom CommSemiRingCat.ofHom
326326

327327
@[simp]
328-
lemma RingEquiv_coe_eq {X Y : Type*} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
328+
lemma RingEquiv_coe_eq {X Y : Type _} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
329329
(@FunLike.coe (CommSemiRingCat.of X ⟶ CommSemiRingCat.of Y) _
330330
(fun _ => (forget CommSemiRingCat).obj _)
331331
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
@@ -441,7 +441,7 @@ set_option linter.uppercaseLean3 false in
441441
#align CommRing.of_hom CommRingCat.ofHom
442442

443443
@[simp]
444-
lemma RingEquiv_coe_eq {X Y : Type*} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
444+
lemma RingEquiv_coe_eq {X Y : Type _} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
445445
(@FunLike.coe (CommRingCat.of X ⟶ CommRingCat.of Y) _ (fun _ => (forget CommRingCat).obj _)
446446
ConcreteCategory.funLike (e : X →+* Y) : X → Y) = ↑e :=
447447
rfl
@@ -600,7 +600,7 @@ theorem CommRingCat.comp_eq_ring_hom_comp {R S T : CommRingCat} (f : R ⟶ S) (g
600600
set_option linter.uppercaseLean3 false in
601601
#align CommRing.comp_eq_ring_hom_comp CommRingCat.comp_eq_ring_hom_comp
602602

603-
theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
603+
theorem CommRingCat.ringHom_comp_eq_comp {R S T : Type _} [CommRing R] [CommRing S] [CommRing T]
604604
(f : R →+* S) (g : S →+* T) : g.comp f = CommRingCat.ofHom f ≫ CommRingCat.ofHom g :=
605605
rfl
606606
set_option linter.uppercaseLean3 false in

‎Mathlib/Algebra/Category/Ring/Instances.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ instance localization_unit_isIso' (R : CommRingCat) :
2727
exact localization_unit_isIso _
2828
#align localization_unit_is_iso' localization_unit_isIso'
2929

30-
theorem IsLocalization.epi {R : Type*} [CommRing R] (M : Submonoid R) (S : Type*) [CommRing S]
30+
theorem IsLocalization.epi {R : Type*} [CommRing R] (M : Submonoid R) (S : Type _) [CommRing S]
3131
[Algebra R S] [IsLocalization M S] : Epi (CommRingCat.ofHom <| algebraMap R S) :=
3232
⟨fun {T} _ _ => @IsLocalization.ringHom_ext R _ M S _ _ T _ _ _ _⟩
3333
#align is_localization.epi IsLocalization.epi

‎Mathlib/Algebra/Category/SemigroupCat/Basic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ theorem coe_of (R : Type u) [Mul R] : (MagmaCat.of R : Type u) = R :=
9797
#align AddMagma.coe_of AddMagmaCat.coe_of
9898

9999
@[to_additive (attr := simp)]
100-
lemma MulEquiv_coe_eq {X Y : Type*} [Mul X] [Mul Y] (e : X ≃* Y) :
100+
lemma MulEquiv_coe_eq {X Y : Type _} [Mul X] [Mul Y] (e : X ≃* Y) :
101101
(@FunLike.coe (MagmaCat.of X ⟶ MagmaCat.of Y) _ (fun _ => (forget MagmaCat).obj _)
102102
ConcreteCategory.funLike (e : X →ₙ* Y) : X → Y) = ↑e :=
103103
rfl
@@ -182,7 +182,7 @@ theorem coe_of (R : Type u) [Semigroup R] : (SemigroupCat.of R : Type u) = R :=
182182
#align AddSemigroup.coe_of AddSemigroupCat.coe_of
183183

184184
@[to_additive (attr := simp)]
185-
lemma MulEquiv_coe_eq {X Y : Type*} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
185+
lemma MulEquiv_coe_eq {X Y : Type _} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
186186
(@FunLike.coe (SemigroupCat.of X ⟶ SemigroupCat.of Y) _ (fun _ => (forget SemigroupCat).obj _)
187187
ConcreteCategory.funLike (e : X →ₙ* Y) : X → Y) = ↑e :=
188188
rfl

‎Mathlib/Algebra/DirectLimit.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -274,7 +274,7 @@ namespace AddCommGroup
274274
variable [∀ i, AddCommGroup (G i)]
275275

276276
/-- The direct limit of a directed system is the abelian groups glued together along the maps. -/
277-
def DirectLimit (f : ∀ i j, i ≤ j → G i →+ G j) : Type* :=
277+
def DirectLimit (f : ∀ i j, i ≤ j → G i →+ G j) : Type _ :=
278278
@Module.DirectLimit ℤ _ ι _ _ G _ _ fun i j hij => (f i j hij).toIntLinearMap
279279
#align add_comm_group.direct_limit AddCommGroup.DirectLimit
280280

‎Mathlib/Algebra/DirectSum/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ variable (ι : Type v) [dec_ι : DecidableEq ι] (β : ι → Type w)
3232
/-- `DirectSum β` is the direct sum of a family of additive commutative monoids `β i`.
3333
3434
Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum β`. -/
35-
def DirectSum [∀ i, AddCommMonoid (β i)] : Type* :=
35+
def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
3636
-- Porting note: Failed to synthesize
3737
-- Π₀ i, β i deriving AddCommMonoid, Inhabited
3838
-- See https://github.com/leanprover-community/mathlib4/issues/5020

0 commit comments

Comments
 (0)