Changes

Summary

fixed proofs
fixed proofs
fixed proofs
merged
moved to analysis
added Johannes' generalizations on Modules.thy and Vector_Spaces.thy; adapted Rank_Nullity, Gauss_Jordan, and QR_Decomposition

Changeset 9173:2ff575ed6160 by immler: fixed proofs
The file was modified	`thys/Echelon_Form/Cayley_Hamilton_Compatible.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/DL_Rank.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_NatInf.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetIntervalStep.thy` (diff)
Changeset 9172:3e378f0be066 by immler: fixed proofs
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy` (diff)
Changeset 9171:12fec0939648 by immler: fixed proofs
The file was modified	`thys/Gauss_Jordan/Inverse.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
Changeset 9170:133a99f555a5 by immler: merged
Changeset 9169:385ddc7c984a by immler: moved to analysis
The file was modified	`thys/Affine_Arithmetic/Executable_Euclidean_Space.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Floatarith_Expression.thy` (diff)
The file was modified	`thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Bell_Numbers.thy` (diff)
The file was modified	`thys/Card_Partitions/Set_Partition.thy` (diff)
The file was modified	`thys/Category/Cat.thy` (diff)
The file was modified	`thys/Category2/Category.thy` (diff)
The file was modified	`thys/Category3/Category.thy` (diff)
The file was modified	`thys/Deep_Learning/Lebesgue_Functional.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Series.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/PRF_IND_CPA.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Bases_Of_Fundamental_Subspaces_IArrays.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Matrix.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Examples_Gauss_Jordan_Abstract.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Linear_Maps.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Rank.thy` (diff)
The file was modified	`thys/Gauss_Jordan/System_Of_Equations.thy` (diff)
The file was modified	`thys/Graph_Theory/Funpow.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra1.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/Logic.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt.thy` (diff)
The file was modified	`thys/QR_Decomposition/Least_Squares_Approximation.thy` (diff)
The file was modified	`thys/QR_Decomposition/Miscellaneous_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Projections.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
The file was modified	`thys/Topology/Topology.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Preliminaries.thy` (diff)
The file was modified	`thys/VectorSpace/FunctionLemmas.thy` (diff)
The file was removed	`thys/Rank_Nullity_Theorem/Cartesian_Space.thy`
The file was removed	`thys/Rank_Nullity_Theorem/Hull.thy`
The file was removed	`thys/Rank_Nullity_Theorem/Modules.thy`
The file was removed	`thys/Rank_Nullity_Theorem/Vector_Spaces.thy`
Changeset 9168:5bbb50b7f616 by immler: added Johannes' generalizations on Modules.thy and Vector_Spaces.thy; adapted Rank_Nullity, Gauss_Jordan, and QR_Decomposition
The file was added	`thys/Rank_Nullity_Theorem/Cartesian_Space.thy`
The file was added	`thys/Rank_Nullity_Theorem/Hull.thy`
The file was added	`thys/Rank_Nullity_Theorem/Modules.thy`
The file was added	`thys/Rank_Nullity_Theorem/Vector_Spaces.thy`
The file was modified	`thys/Gauss_Jordan/Bases_Of_Fundamental_Subspaces.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Examples_Gauss_Jordan_Abstract.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Inverse.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Linear_Maps.thy` (diff)
The file was modified	`thys/Gauss_Jordan/System_Of_Equations.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt.thy` (diff)
The file was modified	`thys/QR_Decomposition/Least_Squares_Approximation.thy` (diff)
The file was modified	`thys/QR_Decomposition/Miscellaneous_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Projections.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
The file was removed	`thys/Rank_Nullity_Theorem/Generalizations.thy`