OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumScalarFaithful.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The four rational registers faithfully represent their complex value. This permits exact local-table identities to reuse the established complex matrix identities, without changing the arithmetic program.

  1. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sqrtHalf_irrational line 12
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_injective line 16
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_injective line 35
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.scalar_eq_iff line 43