English
If B is a singleton (Unique B), then the map (A × B) ≃ₐ[R] A is given by (a,b) ↦ a with inverse a ↦ (a, b0). This again shows the trivial factor on the right does not change the structure.
Русский
Если B — единичный элемент, то карта (A × B) ≃ₐ[R] A задаётся отображением (a,b) ↦ a с обратной стороной a ↦ (a, b0).
LaTeX
$$$$ (A \\times B) \\cong_R A \\quad \\text{при } [Unique B], $$$$
Lean4
/-- Multiplying by the trivial algebra from the left does not change the structure.
This is the `AlgEquiv` version of `LinearEquiv.uniqueProd` and `RingEquiv.zeroRingProd.symm`.
-/
@[simps!]
def uniqueProd [Unique B] : (B × A) ≃ₐ[R] A where
toFun := Prod.snd
invFun x := (0, x)
__ := (RingEquiv.zeroRingProd A B).symm
commutes' _ := rfl
