Theorems · Definition · category theory

ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing

{R : Type u} → [inst : CommRing R] → (A : ModuleCat R) → [CategoryTheory.MonObj A] → Ring ↑A

The ring structure on a monoid object. This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back to a ring, since the npow field is lost in the middle. Therefore, it is scoped.

Defined in

Mathlib.CategoryTheory.Monoidal.Internal.Module

Cited by

2 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCategoryTheory.MonObj