Basic

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

Statistics

Metric	Count
Definitions fintype	1
Theorems of_basis	1
Total	2

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_basis 📖	mathematical	—	Module.Finite	—	nonempty_fintype Finset.coe_image Finset.coe_univ Set.image_univ Module.Basis.span_eq

Module.Free.ChooseBasisIndex

Definitions

Name	Category	Theorems
fintype 📖	CompOp	5 math math: LinearMap.charpoly_def, NumberField.det_basisOfFractionalIdeal_eq_absNorm, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, Module.finrank_eq_card_chooseBasisIndex, NumberField.coe_discr

---

← Back to Index