FormCardinality.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cardinality and dimension of actual symmetric multilinear forms

The coefficient count is transported through the proved linear equivalence with permutation-invariant multilinear maps. No extra representation or symmetry hypothesis is assumed. Nat.card avoids choosing a global Fintype instance for the invariant-map submodule.

theorem OAI.MetricEntropyDuality.SymmetricForm.card line 23
Source documentation
The cardinality of the coefficient carrier.
```
theorem card (p r j : ℕ) [NeZero p] :
    Fintype.card (SymmetricForm (ZMod p) r j) = p ^ formDimension r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.SymmetricForm.finrank_invariantMultilinearSubmodule line 29
Source documentation
Actual permutation-invariant multilinear maps have the same dimension as their freely specified multiset coefficients.
```
theorem finrank_invariantMultilinearSubmodule (K : Type uK) [Field K] (r j : ℕ) :
    Module.finrank K (invariantMultilinearSubmodule K r j) = formDimension r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule, OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.SymmetricForm.natCard_invariantMultilinearSubmodule line 36
Source documentation
The actual invariant multilinear maps over ZMod p have cardinality p raised to the symmetric-form dimension.
```
theorem natCard_invariantMultilinearSubmodule (p r j : ℕ) [NeZero p] :
    Nat.card (invariantMultilinearSubmodule (ZMod p) r j) =
      p ^ formDimension r j := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm.invariantMultilinearSubmodule, OAI.MetricEntropyDuality.formDimension
theorem OAI.MetricEntropyDuality.card_symmetricForm line 50
Source documentation
The cardinality of the symmetric-form coefficient space.
```
theorem card_symmetricForm (p r j : ℕ) [NeZero p] :
    Fintype.card (SymmetricForm (ZMod p) r j) = p ^ formDimension r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.formDimension