Session Free-Groups
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.FuncSet
HOL-Algebra.Congruence
HOL-Algebra.Order
HOL-Algebra.Lattice
HOL-Algebra.Complete_Lattice
HOL-Algebra.Group
HOL-Proofs-Lambda.Commutation
Cancelation
Generators
FreeGroups
UnitGroup
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
HOL-Computational_Algebra.Factorial_Ring
HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Computational_Algebra.Primes
HOL-Algebra.FiniteProduct
HOL-Algebra.Ring
File ‹ringsimp.ML›
HOL-Algebra.Coset
HOL-Algebra.AbelCoset
HOL-Algebra.Ideal
HOL-Algebra.RingHom
HOL-Algebra.QuotRing
HOL-Algebra.IntRing
C2
HOL-Cardinals.Fun_More
HOL-Cardinals.Order_Relation_More
HOL-Cardinals.Wellfounded_More
HOL-Cardinals.Wellorder_Relation
HOL-Cardinals.Wellorder_Embedding
HOL-Cardinals.Order_Union
HOL-Cardinals.Wellorder_Constructions
HOL-Cardinals.Cardinal_Order_Relation
Isomorphisms
HOL-Algebra.Bij
PingPongLemma