Theorems · Definition · functional analysis
IsRCLikeNormedField.rclike
(𝕜 : Type u_3) → [hk : NormedField 𝕜] → [h : IsRCLikeNormedField 𝕜] → RCLike 𝕜
Given a normed field 𝕜 satisfying IsRCLikeNormedField 𝕜, build an associated RCLike 𝕜
structure on 𝕜 which is definitionally compatible with the given normed field structure.
- Defined in
- Mathlib.Analysis.RCLike.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- NormedFieldstatement and proof · cited by 1,084
- IsRCLikeNormedFieldstatement and proof · cited by 104
- RCLike.copy_of_normedFieldproof · cited by 0
- IsRCLikeNormedField.outproof · cited by 0
Cited by32
Results whose statement or proof uses this declaration.
- Convex.norm_image_sub_le_of_norm_hasFDerivWithin_leproof · cited by 9
- ModelWithCorners.uniqueDiffOnproof · cited by 7
- hasStrictFDerivAt_uncurry_coprodproof · cited by 5
- ModelWithCorners.convex_rangeproof · cited by 5
- hasFDerivAt_of_tendstoUniformlyOnFilterproof · cited by 2
- UniqueDiffWithinAt.of_realproof · cited by 2
- second_derivative_symmetric_of_eventuallyproof · cited by 2
- hasFDerivAt_tsumproof · cited by 2
- ModelWithCorners.range_subset_closure_interiorproof · cited by 2
- ModelWithCorners.convex_range'statement · cited by 2
- uniformCauchySeqOn_ball_of_fderivproof · cited by 2
- ModelWithCorners.mk.injstatement · cited by 1