Theorems · Theorem · order theory

Archimedean.embedReal_apply

∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] [inst_3 : One M]
  [inst_4 : ZeroLEOneClass M] [inst_5 : NeZero 1] [inst_6 : Archimedean M] (a : M),
  (Archimedean.embedReal M) a = Archimedean.embedRealFun a

Defined in: Mathlib.Data.Real.Embedding
Cited by: 1 results in Mathlib
Foundations: Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup LinearOrder IsOrderedAddMonoid One ZeroLEOneClass NeZero Archimedean

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

DFunLike.coestatement and proof · cited by 62,936
Realstatement · cited by 25,697
AddCommGroupstatement and proof · cited by 12,871
LinearOrderstatement and proof · cited by 8,572
IsOrderedAddMonoidstatement and proof · cited by 1,659
Archimedeanstatement and proof · cited by 603
ZeroLEOneClassstatement and proof · cited by 304
OrderAddMonoidHomstatement · cited by 80
Archimedean.embedRealstatement and proof · cited by 4
Archimedean.embedRealFunstatement · cited by 4

Cited by1

Results whose statement or proof uses this declaration.

Archimedean.embedReal_oneproof · cited by 0