Theorems · Theorem · group theory

SymplecticGroup.map_mem

∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R} {F : Type u_3} {S : Type u_4} [inst_3 : CommRing S] [inst_4 : FunLike F R S]
  [RingHomClass F R S], A ∈ Matrix.symplecticGroup l R → ∀ (f : F), A.map ⇑f ∈ Matrix.symplecticGroup l S

Defined in

Mathlib.LinearAlgebra.SymplecticGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRingCommRingFunLikeRingHomClass