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_ringEquiv, infinite, instFaithfulSMulOfNontrivial, instIsTorsionFree, instNonemptyChooseBasisIndexOfNontrivial, of_basis, of_equiv, of_equiv', of_ringEquiv, of_subsingleton, of_subsingleton', self, ulift, free_def, free_iff_set	22
Total	26

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 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	LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid 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 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 smulLeft	—	mem_center_iff

Module.Free

Definitions

Name	Category	Theorems
ChooseBasisIndex 📖	CompOp	33 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, rank_eq_card_chooseBasisIndex, NumberField.house.basis_repr_norm_le_const_mul_house, instNonemptyChooseBasisIndexOfNontrivial, NumberField.mixedEmbedding.mem_rat_span_latticeBasis
chooseBasis 📖	CompOp	1 math math: LinearMap.charpoly_def
constr 📖	CompOp	—
instDecidableEqChooseBasisIndex 📖	CompOp	4 math math: LinearMap.charpoly_def, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.coe_discr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_basis 📖	mathematical	—	Module.Basis	—	—
exists_set 📖	mathematical	—	Module.Basis Set.Elem	—	exists_basis
iff_of_ringEquiv 📖	mathematical	—	Module.Free	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv of_ringEquiv
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 of_basis
of_equiv' 📖	mathematical	—	Module.Free	—	RingHomInvPair.ids of_equiv
of_ringEquiv 📖	mathematical	—	Module.Free	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingHomInvPair.of_ringEquiv RingHomInvPair.ids RingHomCompTriple.right_ids RingHomCompTriple.ids AddEquiv.map_add' Finsupp.ext RingEquivClass.toAddEquivClass MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul map_mul NonUnitalRingHomClass.toMulHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.apply_symm_apply Equiv.left_inv Equiv.right_inv of_basis
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