Mathlib Map

Theorems · Definition · functional analysis

RCLike.I

{K : semiOutParam (Type u_1)} → [self : RCLike K] → K

Imaginary unit in K. Meant to be set to 0 for K = ℝ.

Defined in
Mathlib.Analysis.RCLike.Basic
Cited by
100 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
RCLike
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

RCLike.re_add_im · cited by 21RCLike.re_add_imRCLike.I_re · cited by 19RCLike.I_reLinearIsometry.inner_map_map · cited by 16LinearIsometry.inner_map_…RCLike.map · cited by 14RCLike.mapModule.Dual.extendRCLike · cited by 12Dual.extendRCLikeRCLike.map_apply · cited by 12RCLike.map_applyRCLike.complexRingEquiv · cited by 10RCLike.complexRingEquivStrongDual.re_extendRCLike_apply · cited by 9StrongDual.re_extendRCLik…RCLike.I_eq_zero_or_im_I_eq_one · cited by 8RCLike.I_eq_zero_or_im_I_…RCLike.conj_I · cited by 7RCLike.conj_IRCLike.complexRingEquiv_apply · cited by 5RCLike.complexRingEquiv_a…RCLike.im_eq_zero · cited by 5RCLike.im_eq_zeroRCLike.is_real_TFAE · cited by 5RCLike.is_real_TFAERCLike.realRingEquiv · cited by 5RCLike.realRingEquivRCLike.I_im' · cited by 4RCLike.I_im'RCLike · cited by 2829RCLikeRCLike.ICITED BYCITES

Cites1

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

  • RCLikestatement and proof · cited by 2,829

Cited by107

Results whose statement or proof uses this declaration.