def familyPow {A : Type u_1} {G : Type u_2} [CommMonoid A] [Zero G] [Pow A G] {ι : Type u_3} (f : ι → A) (v : ι →₀ G) : A

Equations

• familyPow f v = v.prod fun (i : ι) (k : G) => f i ^ k

def instFamilyPow {A : Type u_1} {G : Type u_2} [CommMonoid A] [Zero G] [Pow A G] {ι : Type u_3} : HPow (ι → A) (ι →₀ G) A

Equations

• instFamilyPow = { hPow := fun (f : ι → A) (v : ι →₀ G) => familyPow f v }

theorem familyPow_def {A : Type u_1} {G : Type u_2} [CommMonoid A] [Zero G] [Pow A G] {ι : Type u_3} (f : ι → A) (v : ι →₀ G) : f ^ v = v.prod fun (i : ι) (k : G) => f i ^ k

theorem familyPow_add {A : Type u_1} [CommMonoid A] {ι : Type u_3} (f : ι → A) (v w : ι →₀ ℕ) : f ^ (v + w) = f ^ v * f ^ w

@[simp]

theorem familyPow_zero {A : Type u_1} [CommMonoid A] {ι : Type u_3} (f : ι → A) : f ^ 0 = 1

theorem Ideal.familyPow_def {A : Type u_1} [CommSemiring A] {ι : Type u_2} (F : ι → Ideal A) (v : ι →₀ ℕ) : F ^ v = v.prod fun (i : ι) (k : ℕ) => F i ^ k

theorem Ideal.mem_familyPow_add {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} {v w : ι →₀ ℕ} {x y : A} (hx : x ∈ F ^ v) (hy : y ∈ F ^ w) : x * y ∈ F ^ (v + w)

theorem Ideal.mem_familyPow_of_mem {A : Type u_1} [CommSemiring A] {ι : Type u_2} {F : ι → Ideal A} {a : ι → A} {v : ι →₀ ℕ} (mem : ∀ i ∈ v.support, a i ∈ F i) : a ^ v ∈ F ^ v