Mathlib Map

Structures · Analysis

RCLike

This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.

Defined in
Mathlib.Analysis.RCLike.Basic
Shape
One type argument · adds re, im, I, I_re_ax, I_mul_I_ax, re_add_im_ax, ofReal_re_ax, ofReal_im_ax, mul_re_ax, mul_im_ax, conj_re_ax, conj_im_ax, conj_I_ax, norm_sq_eq_def_ax, mul_im_I_ax, toPartialOrder, le_iff_re_im, toDecidableEq
Open in Mathlib docs

Extends4

Extended by0

Nothing extends this class yet.

Forgetful instances

Every RCLike is also a

Concrete types that are instances2

  • Real
  • Complex

How is a type an instance?

Loading the hierarchy index…

Assumed by3,119

Ancestors166