@[reducible, inline]
noncomputable abbrev
PhiMap
{A : Type u_1}
{B : Type u_2}
[starAlgebra B]
[starAlgebra A]
[QuantumSet A]
[QuantumSet B]
:
Equations
Instances For
theorem
PhiMap_apply
{A : Type u_1}
{B : Type u_2}
[starAlgebra B]
[starAlgebra A]
[QuantumSet A]
[QuantumSet B]
(f : A →ₗ[ℂ] B)
:
theorem
oneInner_map_one_eq_oneInner_Psi_map
{A : Type u_1}
{B : Type u_2}
[starAlgebra B]
[starAlgebra A]
[hA : QuantumSet A]
[hB : QuantumSet B]
(f : A →ₗ[ℂ] B)
(r t : ℝ)
:
theorem
oneInner_map_one_eq_oneInner_PhiMap_map_one
{A : Type u_1}
{B : Type u_2}
[starAlgebra B]
[starAlgebra A]
[hA : QuantumSet A]
[hB : QuantumSet B]
(f : A →ₗ[ℂ] B)
: