Theorems · Theorem · commutative algebra

map_wittStructureInt

∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) =
    wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n

Defined in

Mathlib.RingTheory.WittVector.StructurePolynomial

Cited by

13 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact