Theorems · Theorem · geometry

ContinuousAffineMap.snd_decompLinearEquiv

∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W]
  (f : V →ᴬ[R] W), ((ContinuousAffineMap.decompLinearEquiv R S V W) f).2 = f.contLinear

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupAddCommGroupModuleTopologicalSpaceModuleSMulCommClassContinuousConstSMulIsTopologicalAddGroup