Mathlib Map

Theorems · Theorem · functional analysis

ContinuousLinearMap.toBilinForm_injective

∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E], Function.Injective ContinuousLinearMap.toBilinForm
Defined in
Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Cited by
1 results in Mathlib
Foundations
Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldAddCommGroupModuleTopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContinuousLinearMap.toBilinForm_inj · cited by 3ContinuousLinearMap.toBil…TopologicalSpace · cited by 24529TopologicalSpaceModule · cited by 20661ModuleRingHom.id · cited by 18349RingHom.idAddCommGroup · cited by 12871AddCommGroupContinuousLinearMap · cited by 5352ContinuousLinearMapNormedField · cited by 1084NormedFieldLinearMap.BilinForm · cited by 501LinearMap.BilinFormContinuousLinearMap.toBilinForm · cited by 10ContinuousLinearMap.toBil…ContinuousLinearMap.toLinearMap₁₂_injective · cited by 2ContinuousLinearMap.toLin…ContinuousLinearMap.toBilinFo…CITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.