Session Projective_Measurements
View
theory dependencies
View
document
View
outline
Theories
Polynomial_Interpolation.Ring_Hom
Jordan_Normal_Form.Missing_Misc
HOL-Algebra.Congruence
HOL-Algebra.Order
HOL-Algebra.Lattice
HOL-Algebra.Complete_Lattice
HOL-Algebra.Group
HOL-Algebra.FiniteProduct
HOL-Algebra.Ring
File ‹ringsimp.ML›
Jordan_Normal_Form.Missing_Ring
Jordan_Normal_Form.Conjugate
HOL-Algebra.Module
Jordan_Normal_Form.Matrix
HOL-Library.More_List
HOL-Computational_Algebra.Polynomial
HOL-Computational_Algebra.Fraction_Field
HOL-Computational_Algebra.Normalized_Fraction
HOL-Computational_Algebra.Polynomial_Factorial
Polynomial_Interpolation.Missing_Unsorted
Polynomial_Interpolation.Missing_Polynomial
Polynomial_Factorization.Order_Polynomial
HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Polynomial_Interpolation.Ring_Hom_Poly
Jordan_Normal_Form.Gauss_Jordan_Elimination
Jordan_Normal_Form.Column_Operations
Jordan_Normal_Form.Determinant
Jordan_Normal_Form.Char_Poly
Jordan_Normal_Form.Jordan_Normal_Form
Isabelle_Marries_Dirac.Basics
Isabelle_Marries_Dirac.Binary_Nat
Isabelle_Marries_Dirac.Quantum
HOL-Algebra.Coset
VectorSpace.RingModuleFacts
VectorSpace.FunctionLemmas
VectorSpace.MonoidSums
VectorSpace.LinearCombinations
VectorSpace.SumSpaces
VectorSpace.VectorSpace
Isabelle_Marries_Dirac.Complex_Vectors
Matrix.Utility
Regular-Sets.Regular_Set
Regular-Sets.Regular_Exp
Regular-Sets.NDerivative
HOL-Library.While_Combinator
Regular-Sets.Equivalence_Checking
Regular-Sets.Relation_Interpretation
Regular-Sets.Regexp_Method
Abstract-Rewriting.Seq
Abstract-Rewriting.Abstract_Rewriting
Abstract-Rewriting.SN_Orders
Matrix.Ordered_Semiring
Matrix.Matrix_Legacy
Matrix_Tensor.Matrix_Tensor
Isabelle_Marries_Dirac.Tensor
Isabelle_Marries_Dirac.More_Tensor
Jordan_Normal_Form.Missing_VectorSpace
Jordan_Normal_Form.VS_Connect
Jordan_Normal_Form.Gram_Schmidt
Jordan_Normal_Form.Schur_Decomposition
Jordan_Normal_Form.Jordan_Normal_Form_Existence
QHLProver.Complex_Matrix
File ‹mat_alg.ML›
QHLProver.Gates
HOL-Types_To_Sets.Prerequisites
HOL-Types_To_Sets.Types_To_Sets
File ‹local_typedef.ML›
File ‹unoverloading.ML›
File ‹internalize_sort.ML›
File ‹unoverload_type.ML›
File ‹unoverload_def.ML›
HOL-Types_To_Sets.Group_On_With
Linear_Algebra_Complements
Projective_Measurements
CHSH_Inequality