English
Let f be a linear equivalence between A ⊗_R B ⊗_R C and D, together with compatibility data h_mul and h_one ensuring the algebra structure is preserved. The algebra isomorphism algEquivOfLinearEquivTripleTensorProduct f h_mul h_one acts on x by sending it to f(x). In other words, the underlying map of this algebra isomorphism is exactly f.
Русский
Пусть f — линейное эквивалентное отображение между A ⊗_R B ⊗_R C и D, совместимое с умножением и единицей посредством данных h_mul и h_one. Получаемый алгебраический изоморфизм algEquivOfLinearEquivTripleTensorProduct f h_mul h_one действует на элементе x как f(x). Иными словами, соответствующее отображение равняется данному линейному эквиваленту.
LaTeX
$$$(\\mathrm{AlgEquivOfLinearEquivTripleTensorProduct}(f, h_{mul}, h_{one}))(x) = f(x) \\quad \\text{for all } x \\in A \\otimes_R B \\otimes_R C.$$$
Lean4
@[simp]
theorem algEquivOfLinearEquivTripleTensorProduct_apply (f h_mul h_one x) :
(algEquivOfLinearEquivTripleTensorProduct f h_mul h_one : A ⊗[R] B ⊗[R] C ≃ₐ[R] D) x = f x :=
rfl
