OAI/Algebra/DepthFive/ImmMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.map_imm line 11

   Source documentation

   Iterated matrix multiplication commutes with change of coefficient semiring.

   @[simp] theorem map_imm {K : Type u} {L : Type v} [CommSemiring K] [CommSemiring L]
       (f : K →+* L) (n : ℕ) : MvPolynomial.map f (imm K n) = imm L n := by
   …

   Mentions: OAI.Problem335.imm