Theorems · Definition · commutative algebra

RingEquiv.subringCongr

{R : Type u} → [inst : NonAssocRing R] → {s t : Subring R} → s = t → ↥s ≃+* ↥t

Makes the identity isomorphism from a proof two subrings of a multiplicative monoid are equal.

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

3 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

NonAssocRing