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