feat: ℕ+ powers in semigroups

Mathlib.lean

@@ -427,6 +427,8 @@ public import Mathlib.Algebra.Group.Nat.Units
 public import Mathlib.Algebra.Group.NatPowAssoc
 public import Mathlib.Algebra.Group.Opposite
 public import Mathlib.Algebra.Group.PNatPowAssoc
+public import Mathlib.Algebra.Group.PPow.Basic
+public import Mathlib.Algebra.Group.PPow.Defs
 public import Mathlib.Algebra.Group.PUnit
 public import Mathlib.Algebra.Group.Pi.Basic
 public import Mathlib.Algebra.Group.Pi.Lemmas

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -387,11 +387,15 @@ instance {K : Type*} [AddMonoid K] [AddAction K H] [VAddAssocClass K H H] :
 instance : Mul (G →+c[a, a] G) := ⟨comp⟩
 instance : One (G →+c[a, a] G) := ⟨.id⟩
 
+instance : Pow (G →+c[a, a] G) ℕ+ where
+  pow f n := ⟨f^[n], Commute.iterate_left (AddConstMapClass.semiconj f) _⟩
+
 instance : Pow (G →+c[a, a] G) ℕ where
   pow f n := ⟨f^[n], Commute.iterate_left (AddConstMapClass.semiconj f) _⟩
 
 instance : Monoid (G →+c[a, a] G) :=
-  DFunLike.coe_injective.monoid (M₂ := Function.End G) _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl
+  DFunLike.coe_injective.monoid (M₂ := Function.End G) _ rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    fun _ _ ↦ rfl
 
 theorem mul_def (f g : G →+c[a, a] G) : f * g = f.comp g := rfl
 @[simp, push_cast] theorem coe_mul (f g : G →+c[a, a] G) : ⇑(f * g) = f ∘ g := rfl
@@ -401,6 +405,8 @@ theorem one_def : (1 : G →+c[a, a] G) = .id := rfl
 
 @[simp, push_cast] theorem coe_pow (f : G →+c[a, a] G) (n : ℕ) : ⇑(f ^ n) = f^[n] := rfl
 
+theorem ppow_apply (f : G →+c[a, a] G) (n : ℕ+) (x : G) : (f ^ n) x = f^[n] x := rfl
+
 theorem pow_apply (f : G →+c[a, a] G) (n : ℕ) (x : G) : (f ^ n) x = f^[n] x := rfl
 
 /-- Coercion to functions as a monoid homomorphism to `Function.End G`. -/

Mathlib/Algebra/AddConstMap/Equiv.lean

@@ -116,6 +116,9 @@ instance instMul : Mul (G ≃+c[a, a] G) := ⟨fun f g ↦ g.trans f⟩
 instance instInv : Inv (G ≃+c[a, a] G) := ⟨.symm⟩
 instance instDiv : Div (G ≃+c[a, a] G) := ⟨fun f g ↦ f * g⁻¹⟩
 
+instance instPowPNat : Pow (G ≃+c[a, a] G) ℕ+ where
+  pow e n := ⟨e^n, (e.toAddConstMap^n).map_add_const'⟩
+
 instance instPowNat : Pow (G ≃+c[a, a] G) ℕ where
   pow e n := ⟨e^n, (e.toAddConstMap^n).map_add_const'⟩
 
@@ -127,7 +130,7 @@ instance instPowInt : Pow (G ≃+c[a, a] G) ℤ where
 
 instance instGroup : Group (G ≃+c[a, a] G) :=
   toEquiv_injective.group _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
-    fun _ _ ↦ rfl
+    (fun _ _ ↦ rfl) fun _ _ ↦ rfl
 
 /-- Projection from `G ≃+c[a, a] G` to permutations `G ≃ G`, as a monoid homomorphism. -/
 @[simps! apply]

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -1094,8 +1094,10 @@ theorem coe_center : (center R A : Set A) = Set.center A :=
   rfl
 
 /-- The center of a non-unital algebra is commutative and associative -/
-instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R A) :=
-  inferInstanceAs <| NonUnitalCommSemiring (NonUnitalSubsemiring.center A)
+instance (priority := 75) center.instNonUnitalCommSemiring :
+    NonUnitalCommSemiring (center R A) where
+  mul_assoc := Subsemigroup.center.commSemigroup.mul_assoc
+  mul_comm := Subsemigroup.center.commSemigroup.mul_comm
 
 instance center.instNonUnitalCommRing {A : Type*} [NonUnitalNonAssocRing A] [Module R A]
     [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing (center R A) :=
@@ -1121,8 +1123,15 @@ end NonUnitalNonAssocSemiring
 variable (R A : Type*) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A]
   [SMulCommClass R A A]
 
--- no instance diamond, as the `npow` field isn't present in the non-unital case.
-example : center.instNonUnitalCommSemiring.toNonUnitalSemiring =
+/-- When the ambient algebra is associative, use the inherited subsemiring structure so that
+positive powers agree definitionally with the ambient powers. -/
+instance center.instNonUnitalCommSemiringOfNonUnitalSemiring :
+    NonUnitalCommSemiring (center R A) where
+  __ := NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A)
+  mul_comm := Subsemigroup.center.commSemigroup.mul_comm
+
+-- no instance diamond
+example : (inferInstance : NonUnitalCommSemiring (center R A)).toNonUnitalSemiring =
     NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A) := by
   with_reducible_and_instances rfl
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -300,9 +300,28 @@ theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) *
 theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i :=
   smul_iSup
 
+instance : Pow (Submodule R A) ℕ+ where
+  pow s n := ppowRec n n.prop s -- as opposed to `s.toAddSubmonoid ^ n`
+
+@[simp]
+protected theorem ppow_zero : M ^ (1 : ℕ+) = M := rfl
+
+protected theorem ppow_succ {n : ℕ+} : M ^ (n + 1) = M ^ n * M := by
+  rcases n with ⟨_|n, hn⟩
+  · contradiction
+  · rfl
+
+private protected theorem ppow_mk_add_two (n : ℕ) :
+    M ^ (PNat.mk (n + 2) (Nat.succ_pos _)) = M ^ (PNat.mk (n + 1) (Nat.succ_pos _)) * M :=
+  rfl
+
 /-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/
 instance : NonUnitalSemiring (Submodule R A) where
   __ := toAddSubmonoid_injective.semigroup _ mul_toAddSubmonoid
+    (fun x n => by
+      induction n using Semigroup.ppow_induction x.toAddSubmonoid with
+      | h1 => simp
+      | hsucc n IH => rw [Submodule.ppow_mk_add_two, mul_toAddSubmonoid, IH])
   zero_mul := bot_mul
   mul_zero := mul_bot
   left_distrib := mul_sup

Mathlib/Algebra/Category/Grp/Preadditive.lean

@@ -36,6 +36,11 @@ instance : Zero (M ⟶ N) where
 
 @[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := rfl
 
+instance : SMul ℕ+ (M ⟶ N) where
+  smul n f := ofHom (n • f.hom)
+
+@[simp] lemma hom_psmul (n : ℕ+) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
+
 instance : SMul ℕ (M ⟶ N) where
   smul n f := ofHom (n • f.hom)
 
@@ -59,6 +64,7 @@ instance : SMul ℤ (M ⟶ N) where
 instance (P Q : AddCommGrpCat) : AddCommGroup (P ⟶ Q) :=
   Function.Injective.addCommGroup (Hom.hom) ConcreteCategory.hom_injective
     rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl)
 
 instance : Preadditive AddCommGrpCat where
 

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -326,6 +326,13 @@ instance : Zero (M ⟶ N) where
 
 @[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := rfl
 
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
+instance : SMul ℕ+ (M ⟶ N) where
+  smul n f := ⟨n • f.hom⟩
+
+@[simp] lemma hom_psmul (n : ℕ+) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
+
 set_option backward.privateInPublic true in
 set_option backward.privateInPublic.warn false in
 instance : SMul ℕ (M ⟶ N) where
@@ -357,6 +364,7 @@ instance : SMul ℤ (M ⟶ N) where
 instance : AddCommGroup (M ⟶ N) :=
   Function.Injective.addCommGroup (Hom.hom) hom_injective
     rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
+      (fun _ _ => rfl)
 
 @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) :
     (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom :=

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -295,6 +295,11 @@ instance : Zero (M ⟶ N) where
 
 @[simp] lemma hom_zero : (0 : M ⟶ N).hom = 0 := rfl
 
+instance : SMul ℕ+ (M ⟶ N) where
+  smul n f := ⟨n • f.hom⟩
+
+@[simp] lemma hom_psmul (n : ℕ+) (f : M ⟶ N) : (n • f).hom = n • f.hom := rfl
+
 instance : SMul ℕ (M ⟶ N) where
   smul n f := ⟨n • f.hom⟩
 
@@ -306,6 +311,7 @@ alias hom_zsmul := hom_nsmul
 
 instance : AddCommMonoid (M ⟶ N) :=
   Function.Injective.addCommMonoid Hom.hom hom_injective rfl (fun _ _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl)
 
 @[simp] lemma hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) :
     (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom :=

Mathlib/Algebra/DirectSum/Ring.lean

@@ -398,7 +398,7 @@ of a `GNonUnitalNonAssocSemiring`. -/
 scoped instance (priority := 900) :
     NonUnitalNonAssocSemiring (A 0) :=
   Function.Injective.nonUnitalNonAssocSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) (map_nsmul _)
+    (of A 0).map_add (of_zero_mul A) (map_psmul _) (map_nsmul _)
 
 /-- The `SMulWithZero` structure on the grade zero part
 of a `GNonUnitalNonAssocSemiring`. -/
@@ -414,6 +414,10 @@ section Semiring
 variable [∀ i, AddCommMonoid (A i)] [AddMonoid ι] [GSemiring A]
 
 @[simp]
+theorem of_zero_ppow (a : A 0) (n : ℕ+) :
+    of A 0 (a ^ n) = of A 0 a ^ n := by
+  induction n using Semigroup.ppow_induction a <;> simp [*, ppow_mk_add_one]
+
 theorem of_zero_pow (a : A 0) : ∀ n : ℕ, of A 0 (a ^ n) = of A 0 a ^ n
   | 0 => by rw [pow_zero, pow_zero, DirectSum.of_zero_one]
   -- Porting note: Lean doesn't think this terminates if we only use `of_zero_pow` alone
@@ -437,7 +441,8 @@ theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 ofNat(n) = ofNat(n) :=
 /-- The `Semiring` structure derived from `GSemiring A`. -/
 scoped instance (priority := 900) : Semiring (A 0) :=
   Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ (of A 0).map_nsmul _ _)
+    (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ (of A 0).map_psmul _ _)
+    (fun _ _ ↦ (of A 0).map_nsmul _ _) (fun _ _ => of_zero_ppow _ _ _)
     (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 
 /-- `of A 0` is a `RingHom`, using the `DirectSum.GradeZero.semiring` structure. -/
@@ -462,7 +467,8 @@ variable [∀ i, AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A]
 /-- The `CommSemiring` structure derived from `GCommSemiring A`. -/
 scoped instance (priority := 900) : CommSemiring (A 0) :=
   Function.Injective.commSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ map_nsmul _ _ _)
+    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ map_psmul _ _ _)
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ => of_zero_ppow _ _ _)
     (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 
 end CommSemiring
@@ -474,8 +480,8 @@ variable [∀ i, AddCommGroup (A i)] [AddZeroClass ι] [GNonUnitalNonAssocSemiri
 /-- The `NonUnitalNonAssocRing` derived from `GNonUnitalNonAssocSemiring A`. -/
 scoped instance (priority := 900) : NonUnitalNonAssocRing (A 0) :=
   Function.Injective.nonUnitalNonAssocRing (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
-    (fun _ _ ↦ map_zsmul _ _ _)
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_psmul _ _ _)
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _)
 
 end Ring
 
@@ -494,8 +500,9 @@ theorem of_intCast (n : ℤ) : of A 0 n = n := by
 /-- The `Ring` derived from `GSemiring A`. -/
 scoped instance (priority := 900) : Ring (A 0) :=
   Function.Injective.ring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
-    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_psmul _ _ _)
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_ppow _ _ _)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 
 end Ring
 
@@ -506,8 +513,9 @@ variable [∀ i, AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A]
 /-- The `CommRing` derived from `GCommSemiring A`. -/
 scoped instance (priority := 900) : CommRing (A 0) :=
   Function.Injective.commRing (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
-    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_psmul _ _ _)
+    (fun _ _ ↦ map_nsmul _ _ _) (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_ppow _ _ _)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 
 end CommRing
 

Mathlib/Algebra/Field/Basic.lean

@@ -224,20 +224,21 @@ noncomputable abbrev Field.ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnit
 end NoncomputableDefs
 
 namespace Function.Injective
-variable [Zero K] [Add K] [Neg K] [Sub K] [One K] [Mul K] [Inv K] [Div K] [SMul ℕ K] [SMul ℤ K]
-  [SMul ℚ≥0 K] [SMul ℚ K] [Pow K ℕ] [Pow K ℤ] [NatCast K] [IntCast K] [NNRatCast K] [RatCast K]
-  (f : K → L) (hf : Injective f)
+variable [Zero K] [Add K] [Neg K] [Sub K] [One K] [Mul K] [Inv K] [Div K] [SMul ℕ+ K] [SMul ℕ K]
+  [SMul ℤ K] [SMul ℚ≥0 K] [SMul ℚ K] [Pow K ℕ+] [Pow K ℕ] [Pow K ℤ] [NatCast K] [IntCast K]
+  [NNRatCast K] [RatCast K] (f : K → L) (hf : Injective f)
 
 /-- Pullback a `DivisionSemiring` along an injective function. -/
 -- See note [reducible non-instances]
 protected abbrev divisionSemiring [DivisionSemiring L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
+    (psmul : ∀ (n : ℕ+) (x), f (n • x) = n • f x) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (ppow : ∀ (x) (n : ℕ+), f (x ^ n) = f x ^ n)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : DivisionSemiring K where
-  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
-  __ := hf.groupWithZero f zero one mul inv div npow zpow
+  toSemiring := hf.semiring f zero one add mul psmul nsmul ppow npow natCast
+  __ := hf.groupWithZero f zero one mul inv div ppow npow zpow
   nnratCast_def q := hf <| by rw [nnratCast, NNRat.cast_def, div, natCast, natCast]
   nnqsmul := (· • ·)
   nnqsmul_def q a := hf <| by rw [nnqsmul, NNRat.smul_def, mul, nnratCast]
@@ -247,15 +248,17 @@ protected abbrev divisionSemiring [DivisionSemiring L] (zero : f 0 = 0) (one : f
 protected abbrev divisionRing [DivisionRing L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y)
+    (div : ∀ x y, f (x / y) = f x / f y) (psmul : ∀ (n : ℕ+) (x), f (n • x) = n • f x)
     (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
     (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
+    (ppow : ∀ (x) (n : ℕ+), f (x ^ n) = f x ^ n)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
     (ratCast : ∀ q : ℚ, f q = q) : DivisionRing K where
-  toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
-  __ := hf.groupWithZero f zero one mul inv div npow zpow
-  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
+  toRing := hf.ring f zero one add mul neg sub psmul nsmul zsmul ppow npow natCast intCast
+  __ := hf.groupWithZero f zero one mul inv div ppow npow zpow
+  __ := hf.divisionSemiring f zero one add mul inv div psmul nsmul nnqsmul ppow npow zpow natCast
+    nnratCast
   ratCast_def q := hf <| by rw [ratCast, div, intCast, natCast, Rat.cast_def]
   qsmul := (· • ·)
   qsmul_def q a := hf <| by rw [qsmul, mul, Rat.smul_def, ratCast]
@@ -265,28 +268,31 @@ protected abbrev divisionRing [DivisionRing L] (zero : f 0 = 0) (one : f 1 = 1)
 protected abbrev semifield [Semifield L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
-    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x)
+    (psmul : ∀ (n : ℕ+) (x), f (n • x) = n • f x) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (ppow : ∀ (x) (n : ℕ+), f (x ^ n) = f x ^ n)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q) : Semifield K where
-  toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
-  __ := hf.commGroupWithZero f zero one mul inv div npow zpow
-  __ := hf.divisionSemiring f zero one add mul inv div nsmul nnqsmul npow zpow natCast nnratCast
+  toCommSemiring := hf.commSemiring f zero one add mul psmul nsmul ppow npow natCast
+  __ := hf.commGroupWithZero f zero one mul inv div ppow npow zpow
+  __ := hf.divisionSemiring f zero one add mul inv div psmul nsmul nnqsmul ppow npow zpow natCast
+    nnratCast
 
 /-- Pullback a `Field` along an injective function. -/
 -- See note [reducible non-instances]
 protected abbrev field [Field L] (zero : f 0 = 0) (one : f 1 = 1)
     (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y)
+    (div : ∀ x y, f (x / y) = f x / f y) (psmul : ∀ (n : ℕ+) (x), f (n • x) = n • f x)
     (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
     (nnqsmul : ∀ (q : ℚ≥0) (x), f (q • x) = q • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
+    (ppow : ∀ (x) (n : ℕ+), f (x ^ n) = f x ^ n)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
     (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) (nnratCast : ∀ q : ℚ≥0, f q = q)
     (ratCast : ∀ q : ℚ, f q = q) :
     Field K where
-  toCommRing := hf.commRing f zero one add mul neg sub nsmul zsmul npow natCast intCast
-  __ := hf.divisionRing f zero one add mul neg sub inv div nsmul zsmul nnqsmul qsmul npow zpow
-    natCast intCast nnratCast ratCast
+  toCommRing := hf.commRing f zero one add mul neg sub psmul nsmul zsmul ppow npow natCast intCast
+  __ := hf.divisionRing f zero one add mul neg sub inv div psmul nsmul zsmul nnqsmul qsmul ppow npow
+    zpow natCast intCast nnratCast ratCast
 
 end Function.Injective
 

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -110,8 +110,8 @@ instance (priority := 75) toDivisionRing (s : S) : DivisionRing s := fast_instan
   Subtype.coe_injective.divisionRing ((↑) : s → K)
     rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
     (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
-    (fun _ _ ↦ rfl) (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
-    (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
 
 -- Prefer subclasses of `Field` over subclasses of `SubfieldClass`.
 /-- A subfield of a field inherits a field structure -/
@@ -120,8 +120,8 @@ instance (priority := 75) toField {K} [Field K] [SetLike S K] [SubfieldClass S K
   Subtype.coe_injective.field ((↑) : s → K)
     rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
     (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
-    (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
-    (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
+    (fun _ _ ↦ rfl) (coe_nnqsmul _) (coe_qsmul _) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
+    (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)
 
 end SubfieldClass