Theorems · Theorem · group theory

Matrix.map_J

∀ (l : Type u_1) {R : Type u_2} [inst : DecidableEq l] [inst_1 : CommRing R] {F : Type u_3} {S : Type u_4}
  [inst_2 : CommRing S] [inst_3 : FunLike F R S] [AddMonoidHomClass F R S] [OneHomClass F R S] (f : F),
  (Matrix.J l R).map ⇑f = Matrix.J l S

Defined in

Mathlib.LinearAlgebra.SymplecticGroup

Cited by

1 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

DecidableEqCommRingCommRingFunLikeAddMonoidHomClassOneHomClass