Theorems · Definition · logic and foundations
IsProperLinearSet
{M : Type u_1} → [AddCommMonoid M] → Set M → PropA linear set is proper if its submonoid generators (periods) are linearly independent.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommMonoidstatement and proof · cited by 12,281
- SetLike.coeproof · cited by 8,199
- HVAdd.hVAddproof · cited by 1,820
- Set.Finiteproof · cited by 1,814
- AddSubmonoid.closureproof · cited by 224
- LinearIndepOnproof · cited by 211
Cited by10
Results whose statement or proof uses this declaration.
- IsProperSemilinearSetproof · cited by 10
- isProperSemilinearSet_iffstatement · cited by 1
- isProperLinearSet_iffstatement · cited by 1
- IsProperSemilinearSet.unionproof · cited by 1
- Nat.isSemilinearSet_iff_ultimately_periodicproof · cited by 1
- IsProperLinearSet.isLinearSetstatement and proof · cited by 1
- IsProperLinearSet.isProperSemilinearSetstatement and proof · cited by 1
- IsProperSemilinearSet.emptyproof · cited by 0
- IsProperSemilinearSet.isSemilinearSetproof · cited by 0
- IsProperLinearSet.singletonstatement · cited by 0