English
There exists a commutative ring structure on any nonempty type α.
Русский
Существует коммутативное кольцо на любой непустой множестве α.
LaTeX
$$$\\operatorname{Nonempty}(\\text{CommRing}(\\alpha))$$$
Lean4
/-- A commutative ring can be constructed on any non-empty type.
See also `Infinite.nonempty_field`. -/
instance nonempty_commRing [Nonempty α] : Nonempty (CommRing α) :=
by
obtain hR | hR := finite_or_infinite α
· obtain ⟨x⟩ := nonempty_fintype α
have : NeZero (Fintype.card α) := ⟨by simp⟩
classical
obtain ⟨e⟩ := Fintype.truncEquivFin α
exact ⟨open scoped Fin.CommRing in e.commRing⟩
· have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
exact ⟨e.commRing⟩
