Structures · Algebra
Module.Free
Module.Free R M is the statement that the R-module M is free.
- Defined in
- Mathlib.LinearAlgebra.FreeModule.Basic
- Shape
- 2 explicit arguments · adds exists_basis
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- Int
- Polynomial
- MvPolynomial
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by626
- Module.Free.ChooseBasisIndex
- Ideal.absNorm
- Module.Free.chooseBasis
- LinearMap.charpoly
- LinearMap.polyCharpoly
- Module.Free.exists_basis
- Module.finrank_mul_finrank
- Module.Free.of_equiv
- Module.finBasis
- Module.finrank_eq_card_chooseBasisIndex
- NumberField.HeightOneSpectrum.adicAbv
- FractionalIdeal.absNorm
- Ideal.absNorm_span_singleton
- NumberField.HeightOneSpectrum.absNorm_ne_zero
- Algebra.norm_algebraMap
- LinearMap.nilRank
- Module.Free.rank_eq_card_chooseBasisIndex
- LieAlgebra.rank
- LinearMap.charpoly_toMatrix
- Module.finrank_eq_zero_of_subsingleton
- Module.finite_of_finrank_pos
- NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal
- LieModule.rank
- Module.finrank_of_not_finite
- rank_mul_rank
- Module.rank_lt_aleph0_iff
- Algebra.norm_localization
- LieAlgebra.IsRegular
- Algebra.FormallyUnramified.finite_of_free
- minpoly.natDegree_le
- SpecialLinearGroup.centerEquivRootsOfUnity
- NumberField.FinitePlace.norm_embedding
- Module.finBasisOfFinrankEq
- LinearMap.charpoly_monic
- Module.finrank_tensorProduct
- Module.finrank_pi_fintype
- rank_pi
- Algebra.norm_eq_zero_iff
- LinearMap.aeval_self_charpoly
- Ideal.absNorm_dvd_absNorm_of_le
- NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv
- Algebra.norm_zero
- LieModule.IsRegular
- LinearMap.trace_eq_contract_apply
- Ideal.absNorm_mem
- Ideal.absNorm_apply
- Algebra.trace_trace
- LinearMap.IsNilRegular
- LinearMap.det_smul
- Algebra.norm_norm
Ancestors0
No ancestors.