Theorems · Definition · functional analysis
RCLike.reLm
{K : Type u_1} → [inst : RCLike K] → K →ₗ[ℝ] ℝThe real part in an RCLike field, as a linear map.
- Defined in
- Mathlib.Analysis.RCLike.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RCLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- AddMonoidHomproof · cited by 3,230
- RCLikestatement and proof · cited by 2,829
- RCLike.reproof · cited by 319
- ZeroHom.toFunproof · cited by 101
- AddMonoidHom.toZeroHomproof · cited by 61
- RCLike.smul_reproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- RCLike.reCLMproof · cited by 20
- Module.Dual.extendRCLikeₗproof · cited by 2
- ConvexOn.convex_re_epigraphproof · cited by 1
- Module.Dual.exists_extension_of_le_seminormproof · cited by 1
- Module.Dual.extendRCLikeₗ_symm_applystatement · cited by 0
- RCLike.reCLM_coestatement · cited by 0
- RCLike.reCLM_normproof · cited by 0
- RCLike.reLm_coestatement · cited by 0