Theorems · Definition · commutative algebra
RingEquiv.prodComm
{R : Type u_1} → {S : Type u_3} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R × S ≃+* S × RSwapping components as an equivalence of (semi)rings.
- Defined in
- Mathlib.Algebra.Ring.Prod
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingEquivstatement · cited by 1,147
- MulEquivproof · cited by 1,142
- AddEquivproof · cited by 1,087
- NonAssocSemiringstatement and proof · cited by 805
- AddEquiv.toEquivproof · cited by 174
- AddEquiv.prodCommproof · cited by 5
- MulEquiv.prodCommproof · cited by 5
Cited by7
Results whose statement or proof uses this declaration.
- Ideal.map_prodComm_prodstatement and proof · cited by 2
- RingEquiv.snd_comp_coe_prodCommstatement · cited by 1
- Ideal.isPrime_of_isPrime_prod_top'proof · cited by 1
- RingEquiv.fst_comp_coe_prodCommstatement · cited by 1
- Ideal.isPrime_ideal_prod_top'proof · cited by 1
- RingEquiv.coe_prodCommstatement · cited by 0
- RingEquiv.coe_prodComm_symmstatement · cited by 0