Basic

📁 Source: Mathlib/LinearAlgebra/FreeModule/Basic.lean

Statistics

Metric	Count
Definitions ChooseBasisIndex, chooseBasis, constr, instDecidableEqChooseBasisIndex	4
Theorems repr_algebraMap, mem_center_iff, mem_submonoidCenter_iff, mem_subsemigroupCenter_iff, free_shrink, exists_basis, exists_set, iff_of_equiv, iff_of_ringEquiv, infinite, instFaithfulSMulOfNontrivial, instIsTorsionFree, instNonemptyChooseBasisIndexOfNontrivial, of_basis, of_equiv, of_equiv', of_ringEquiv, of_subsingleton, of_subsingleton', self, ulift, free_def, free_iff_set	23
Total	27

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free_def 📖	mathematical	—	Free Basis	—	Free.exists_basis small_subtype Nonempty.map nonempty_sigma
free_iff_set 📖	mathematical	—	Free Set Basis Set.Elem	—	Free.exists_set nonempty_sigma

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
repr_algebraMap 📖	mathematical	DFunLike.coe Module.Basis CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finsupp.instAddCommMonoid Algebra.toModule Ring.toSemiring Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr RingHom RingHom.instFunLike algebraMap Finsupp.single NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finsupp.ext RingHomInvPair.ids Algebra.algebraMap_eq_smul_one map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass repr_self Finsupp.smul_single mul_one

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_center_iff 📖	mathematical	—	Module.End Set Set.instMembership Set.center instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring smulLeft	—	MulZeroClass.mul_zero MulZeroClass.zero_mul Module.Basis.index_nonempty RingHomInvPair.ids IsScalarTower.left Module.Basis.repr_self Finsupp.single_eq_same one_smul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_one
mem_submonoidCenter_iff 📖	mathematical	—	Module.End Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.center smulLeft	—	mem_center_iff
mem_subsemigroupCenter_iff 📖	mathematical	—	Module.End Subsemigroup instMul SetLike.instMembership Subsemigroup.instSetLike Subsemigroup.center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring smulLeft	—	mem_center_iff

Module.Free

Definitions

Name	Category	Theorems
ChooseBasisIndex 📖	CompOp	34 math math: NumberField.basisMatrix_eq_embeddingsMatrixReindex, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, LinearMap.charpoly_def, NumberField.canonicalEmbedding.mem_span_latticeBasis, NumberField.integralBasis_apply, NumberField.canonicalEmbedding.latticeBasis_apply, NumberField.canonicalEmbedding.integralBasis_repr_apply, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.mem_span_latticeBasis, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.integralBasis_repr_apply, NumberField.mixedEmbedding.span_latticeBasis, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Module.finrank_eq_card_chooseBasisIndex, NumberField.inverse_basisMatrix_mulVec_eq_repr, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, NumberField.mem_span_integralBasis, NumberField.mem_span_basisOfFractionalIdeal, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, NumberField.basisOfFractionalIdeal_apply, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.coe_discr, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Representation.Equiv.dualTensorHom_invFun, rank_eq_card_chooseBasisIndex, NumberField.house.basis_repr_norm_le_const_mul_house, instNonemptyChooseBasisIndexOfNontrivial, NumberField.mixedEmbedding.mem_rat_span_latticeBasis
chooseBasis 📖	CompOp	2 math math: LinearMap.charpoly_def, Representation.Equiv.dualTensorHom_invFun
constr 📖	CompOp	—
instDecidableEqChooseBasisIndex 📖	CompOp	5 math math: LinearMap.charpoly_def, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.coe_discr, Representation.Equiv.dualTensorHom_invFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_basis 📖	mathematical	—	Module.Basis	—	—
exists_set 📖	mathematical	—	Set Module.Basis Set.Elem	—	exists_basis
iff_of_equiv 📖	mathematical	—	Module.Free	—	of_equiv
iff_of_ringEquiv 📖	mathematical	—	Module.Free	—	iff_of_equiv
infinite 📖	mathematical	—	Infinite	—	Equiv.infinite_iff RingHomInvPair.ids Finsupp.infinite_of_right instNonemptyChooseBasisIndexOfNontrivial
instFaithfulSMulOfNontrivial 📖	mathematical	—	FaithfulSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	FaithfulSMul.of_injective RingHomInvPair.ids Finsupp.instFaithfulSMulOfNonempty instNonemptyChooseBasisIndexOfNontrivial instFaithfulSMul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.injective
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree	—	exists_basis Module.Basis.isTorsionFree
instNonemptyChooseBasisIndexOfNontrivial 📖	mathematical	—	ChooseBasisIndex	—	Module.Basis.index_nonempty
of_basis 📖	mathematical	—	Module.Free	—	Module.free_def small_self
of_equiv 📖	mathematical	—	Module.Free	—	RingHomInvPair.ids RingHomCompTriple.right_ids RingHomCompTriple.ids AddEquiv.map_add' Finsupp.ext RingEquivClass.toAddEquivClass RingEquiv.instRingEquivClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RingHomCompTriple.comp_apply RingHomInvPair.triples₂ Equiv.left_inv Equiv.right_inv of_basis
of_equiv' 📖	mathematical	—	Module.Free	—	RingHomInvPair.ids of_equiv
of_ringEquiv 📖	mathematical	—	Module.Free	—	of_equiv
of_subsingleton 📖	mathematical	—	Module.Free	—	of_basis PEmpty.instIsEmpty
of_subsingleton' 📖	mathematical	—	Module.Free	—	of_subsingleton Module.subsingleton
self 📖	mathematical	—	Module.Free NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	of_basis
ulift 📖	mathematical	—	Module.Free ULift.addCommMonoid ULift.module'	—	of_equiv RingHomInvPair.ids

Module.Free.Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
free_shrink 📖	mathematical	—	Module.Free Shrink Shrink.instAddCommMonoid Shrink.instModule	—	Module.Free.of_equiv RingHomInvPair.ids

---

← Back to Index