Main results 101 to 117

Declaration	Kind	Where	Note
AddEquiv.monoidAlgebraMultiplicativeEquivMvLaurentPolynomial_single	theorem	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 44	Forward law: single (ofAdd g) a maps to the Laurent basis term single (e g) a.
AddEquiv.monoidAlgebraMultiplicativeEquivMvLaurentPolynomial_symm_single	theorem	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 60	Inverse law: single m a maps to single (ofAdd (e.symm m)) a.
FreeAbelianGroup.monoidAlgebraEquivMvLaurentPolynomial	def	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 76	Canonical specialization through FreeAbelianGroup.equivFinsupp, under CommSemiring A and arbitrary index type.
FreeAbelianGroup.monoidAlgebraEquivMvLaurentPolynomial_single	theorem	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 84	Forward canonical basis law uses the exponent vector equivFinsupp sigma g.
FreeAbelianGroup.monoidAlgebraEquivMvLaurentPolynomial_symm_single	theorem	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 95	Inverse canonical basis law uses (equivFinsupp sigma).symm m.
FreeAbelianGroup.monoidAlgebraEquivMvLaurentPolynomial_generator	theorem	GroupRings/FreeAbelian/LaurentPolynomial.lean, line 107	The free generator of i maps to exponent Finsupp.single i 1, with arbitrary coefficient a.
AddChar.linearIndependent_field	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 40	Dedekind independence of evaluations AddChar G K into G → K over a field, without finiteness or enough-roots assumptions.
AddChar.finite_of_field	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 56	A finite additive abelian group has finitely many field-valued characters, without an enough-roots assumption.
AddChar.natCard_eq_of_hasEnoughRootsOfUnity	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 63	The dual and G have the same Nat.card given finiteness and enough roots of unity of the group exponent.
AddChar.basisOfEnoughRootsOfUnity	def	GroupRings/FiniteAbelian/RightConvolution.lean, line 71	Character-evaluation basis for G → K under Finite G, Field K and enough roots of unity.
AddChar.coe_basisOfEnoughRootsOfUnity	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 81	Coercion of the basis to functions is precisely evaluation of characters.
AddChar.basisOfEnoughRootsOfUnity_apply	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 90	Each basis vector at psi equals psi as a function on G.
FiniteFourier.rightConvolution	def	GroupRings/FiniteAbelian/RightConvolution.lean, line 102	Matrix indexed by G with entries f (-sigma + tau), under Fintype G and Field K.
FiniteFourier.rightConvolutionEigenvalue	def	GroupRings/FiniteAbelian/RightConvolution.lean, line 105	Positive-character coefficient ∑ x, f x * psi x, without an enough-roots assumption.
FiniteFourier.rightConvolution_mulVec_addChar	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 110	Character eigenvector law for right convolution without requiring enough roots.
FiniteFourier.toMatrix_rightConvolution	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 134	Diagonalization in the character basis; character-index Fintype and DecidableEq remain explicit public binders.
FiniteFourier.rank_rightConvolution	theorem	GroupRings/FiniteAbelian/RightConvolution.lean, line 158	Rank is Nat.card of characters with nonzero positive-character eigenvalue, without a public character Fintype binder.

Quoted from the main results in formalization.yaml of FormalFrontier/group-rings at commit 8e90e656, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.