Theorems · Definition
ULift.ringEquiv
{R : Type u} → [inst : NonUnitalNonAssocSemiring R] → ULift.{u_1, u} R ≃+* RThe ring equivalence between ULift R and R.
- Defined in
- Mathlib.Algebra.Ring.ULift
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- NonUnitalNonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingEquivstatement · cited by 1,147
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
Cited by10
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquivproof · cited by 12
- ULift.algebra'proof · cited by 11
- RingHom.uliftproof · cited by 5
- ULift.algEquivproof · cited by 4
- WittVector.IsPoly.extproof · cited by 2
- WittVector.IsPoly₂.extproof · cited by 1
- RingHom.comp_ulift_eqstatement · cited by 1
- RingHom.Flat.ulift_iffproof · cited by 1
- AlgebraicGeometry.AffineSpace.of_mvPolynomial_int_extproof · cited by 0
- AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_applystatement · cited by 0