FreeAlgebra

📁 Source: Mathlib/LinearAlgebra/FreeAlgebra.lean

Statistics

Metric	Count
Definitions FreeAlgebra, basisFreeMonoid	2
Theorems rank_adjoin_le, instFree, rank_eq	3
Total	5

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_adjoin_le 📖	mathematical	—	Cardinal Cardinal.instLE Module.rank Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Subalgebra.instModuleSubtypeMem SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Set.Elem Cardinal.aleph0	—	adjoin_eq_range_freeAlgebra_lift subsingleton_or_nontrivial rank_subsingleton LE.le.trans Cardinal.one_le_aleph0 le_max_right Cardinal.lift_le RingHomSurjective.ids lift_rank_range_le FreeAlgebra.rank_eq Cardinal.lift_id' Cardinal.lift_umax max_comm Cardinal.mk_list_le_max

FreeAlgebra

Definitions

Name	Category	Theorems
basisFreeMonoid 📖	CompOp	1 math math: Module.Basis.tensorAlgebra_repr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFree 📖	mathematical	—	Module.Free FreeAlgebra CommSemiring.toSemiring instAddCommMonoid Algebra.toModule instSemiring instAlgebra Algebra.id	—	Module.Free.of_equiv MonoidAlgebra.instFree Module.Free.self
rank_eq 📖	mathematical	—	Module.rank FreeAlgebra CommRing.toCommSemiring CommSemiring.toSemiring instAddCommMonoid Algebra.toModule instSemiring instAlgebra Algebra.id Cardinal.lift	—	Module.Basis.mk_eq_rank' commRing_strongRankCondition Cardinal.lift_id Cardinal.lift_umax FreeMonoid.eq_1

(root)

Definitions

Name	Category	Theorems
FreeAlgebra 📖	CompOp	48 math math: FreeAlgebra.lift_comp_ι, TensorAlgebra.ι_def, FreeAlgebra.instFree, FreeAlgebra.star_algebraMap, FreeAlgebra.instSMulCommClass, FreeAlgebra.instIsDomain, TensorAlgebra.equivFreeAlgebra_symm_ι, FreeAlgebra.cardinalMk_le_max, FreeAlgebra.liftAux_eq, FreeAlgebra.ι_injective, FreeAlgebra.cardinalMk_eq_lift, TensorAlgebra.equivFreeAlgebra_ι_apply, FreeAlgebra.lift_ι_apply, FreeAlgebra.star_ι, Algebra.FiniteType.iff_quotient_freeAlgebra, Algebra.adjoin_range_eq_range_freeAlgebra_lift, MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, FreeAlgebra.instNoZeroDivisors, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, FreeAlgebra.toTensor_ι, Algebra.FiniteType.instFreeAlgebraOfFinite, AlgCat.free_obj, FreeAlgebra.rank_eq, FreeAlgebra.algebraMap_inj, FreeAlgebra.ι_comp_lift, FreeAlgebra.adjoin_range_ι, Algebra.FiniteType.iff_quotient_freeAlgebra', FreeAlgebra.lift_unique, Module.Basis.tensorAlgebra_repr_apply, FreeAlgebra.lift_symm_apply, AlgCat.free_map, FreeAlgebra.charZero, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, FreeAlgebra.charP, FreeAlgebra.instNontrivial, FreeAlgebra.cardinalMk_le_max_lift, Algebra.adjoin_eq_range_freeAlgebra_lift, FreeAlgebra.algebraMap_eq_one_iff, FreeAlgebra.cardinalMk_eq_one, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, FreeAlgebra.hom_ext_iff, FreeAlgebra.instIsScalarTower, FreeAlgebra.algebraMap_leftInverse, FreeAlgebra.algebraMap_eq_zero_iff, FreeAlgebra.cardinalMk_eq_max, FreeAlgebra.cardinalMk_eq, AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure, FreeAlgebra.cardinalMk_eq_max_lift

---

← Back to Index