Main results 1 to 100
| Declaration | Kind | Where | Note |
|---|---|---|---|
MonoidAlgebra.ker_mapRingHom_pow_eq_bot_iff |
theorem | GroupRings/MonoidAlgebra/KernelPowers.lean, line 135 | For any homomorphism between independently universed semirings and any monoid, the coefficient-map kernel has zero n-th power iff the coefficient kernel does, at the same n including zero; no commutativity, nontriviality, surjectivity or finiteness. |
MonoidAlgebra.eq_iff_forall_mul_coeff_eq_right |
theorem | GroupRings/MonoidAlgebra/ProductCoefficients.lean, line 37 | For any semiring and group in independent universes, equality is equivalent to equality at one fixed arbitrary coefficient in every right product. Zero and noncommutative coefficients and infinite groups are allowed. |
MonoidAlgebra.eq_iff_forall_mul_coeff_eq_left |
theorem | GroupRings/MonoidAlgebra/ProductCoefficients.lean, line 50 | The separate criterion for every left product, preserving coefficient multiplication order. |
MonoidAlgebra.eq_zero_iff_forall_mul_coeff_eq_zero_right |
theorem | GroupRings/MonoidAlgebra/ProductCoefficients.lean, line 63 | Vanishing of one fixed coefficient in every right product detects the zero element over any semiring. |
MonoidAlgebra.eq_zero_iff_forall_mul_coeff_eq_zero_left |
theorem | GroupRings/MonoidAlgebra/ProductCoefficients.lean, line 68 | The corresponding zero characterization for all left products; index one specializes to identity-coefficient separation without an extra declaration. |
MonoidAlgebra.mem_center_iff |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 126 | For arbitrary semirings and groups in independent universes, centrality is equivalent to central coefficients and conjugation invariance, including zero and noncommutative coefficients. |
MonoidAlgebra.coeff_mem_center |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 70 | Every coefficient of a central monoid-algebra element is central, for any semiring and monoid; no group assumption is needed. |
MonoidAlgebra.coeff_conj_of_mem_center |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 154 | Coefficients of central group-algebra elements are invariant under conjugation. |
MonoidAlgebra.finite_conjAct_orbit_of_coeff_ne_zero |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 163 | A nonzero coefficient of a central element forces that label's canonical conjugation orbit to be finite, not the group to be finite or the label central. |
MonoidAlgebra.coeff_eq_zero_of_not_finite_conjAct_orbit |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 177 | Every coefficient of a central group-algebra element vanishes on an infinite conjugation orbit. |
MonoidAlgebra.mem_center_iff_of_subsingleton |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 184 | For a one-element group, centrality reduces to centrality of the identity coefficient, without commutativity or nontriviality of coefficients. |
MonoidAlgebra.mem_center_iff_coeff_conj |
theorem | GroupRings/MonoidAlgebra/Center.lean, line 205 | For commutative semiring coefficients, centrality is equivalent to conjugation invariance alone. |
MonoidAlgebra.matrixRingEquiv |
def | GroupRings/MonoidAlgebra/Matrix.lean, line 35 | Canonical ring equivalence between a monoid algebra of finite square matrices and matrices of monoid-algebra entries, with forward/inverse coefficient and single-term laws over arbitrary semirings and monoids, including empty matrix indices. |
Ideal.isNoetherian_iff_of_pow_le_annihilator |
theorem | GroupRings/RingTheory/Ideal/ScalarRestriction.lean, line 244 | For arbitrary rings, quotient-surjective scalar restriction and a uniformly nilpotent two-sided ideal action preserve and reflect Noetherianity; exact Module.compHom action and independent universes. |
Ideal.isArtinian_iff_of_pow_le_annihilator |
theorem | GroupRings/RingTheory/Ideal/ScalarRestriction.lean, line 256 | The separate Artinian equivalence under the same hypotheses, without finite generation or finite length. |
Ideal.length_eq_of_pow_le_annihilator |
theorem | GroupRings/RingTheory/Ideal/ScalarRestriction.lean, line 268 | Equality of canonical composition lengths in ENat, including infinity, under the same hypotheses. Nilpotent-ideal corollaries require no module-specific bound. |
MonoidAlgebra.isNoetherian_iff_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/ModuleFiniteness.lean, line 54 | Every module of a finite p-group algebra over any ring with prime p=0 is Noetherian iff its canonical coefficient restriction is. |
MonoidAlgebra.isArtinian_iff_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/ModuleFiniteness.lean, line 69 | The corresponding separate Artinian equivalence for any given module, including noncommutative and zero coefficients. |
MonoidAlgebra.length_eq_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/ModuleFiniteness.lean, line 84 | Canonical ring-relative length over R[G] equals that under moduleCoefficientModule, including infinite length; no field-dimension claim. |
MonoidAlgebra.injective_iff_fixedVectorMap |
theorem | GroupRings/MonoidAlgebra/ModuleDetection.lean, line 161 | Every map of unital modules over any finite p-group algebra with prime p=0 in R is injective iff its canonical fixed-vector map is injective; independent universes, no finite generation, commutativity or nontriviality premise. |
MonoidAlgebra.surjective_iff_coinvariantMap |
theorem | GroupRings/MonoidAlgebra/ModuleDetection.lean, line 169 | Surjectivity iff surjectivity on the original augmentation-ideal-action quotients, with canonical coefficient actions and the same arbitrary-ring finite-p-group hypotheses. |
MonoidAlgebra.isSimpleModule_iff_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/SimpleModules.lean, line 130 | For any Ring R, finite p-group G and unital module V with prime p=0 in R, simplicity over R[G] iff simplicity under the canonical coefficient restriction; independent universes and no extra module hypotheses. |
MonoidAlgebra.smul_eq_augmentation_smul_of_isSimpleModule_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/SimpleModules.lean, line 118 | Every scalar acts on every vector of a simple finite-p-group-algebra module through augmentation and the same coefficient embedding. |
MonoidAlgebra.smul_eq_augmentation_smul_iff |
theorem | GroupRings/MonoidAlgebra/SimpleModules.lean, line 46 | For arbitrary semirings, monoids and semimodules, augmentation action iff every canonical monoid symbol fixes every vector. |
MonoidAlgebra.ker_augmentation_le_torsionOf_iff |
theorem | GroupRings/MonoidAlgebra/FixedVectors.lean, line 40 | For arbitrary rings, monoids and vectors of unital modules, augmentation-kernel annihilation iff canonical-symbol fixedness. |
MonoidAlgebra.exists_ne_zero_fixed_of_isPGroup |
theorem | GroupRings/MonoidAlgebra/FixedVectors.lean, line 93 | Any nontrivial unital module of a finite p-group algebra over any possibly noncommutative ring with prime p=0 has a nonzero canonical fixed vector, with no module finiteness hypothesis. |
MonoidAlgebra.augmentation_pow_card_eq_bot |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence/Finite.lean, line 73 | For a finite p-group over any possibly noncommutative ring with prime p=0, the canonical augmentation kernel has zero Nat.card G-th power, including the zero coefficient ring. |
MonoidAlgebra.augmentation_list_prod_eq_zero |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence/Finite.lean, line 131 | Every ordered mixed product of Nat.card G augmentation elements vanishes under the same all-ring finite-p-group hypotheses. |
MonoidAlgebra.isNilpotent_augmentation_iff_isPGroup |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence/Finite.lean, line 139 | For finite groups over nontrivial rings with prime p=0, canonical ideal nilpotence is equivalent to IsPGroup p G. |
MonoidAlgebra.isNilpotent_of_augmentation_eq_zero |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence/LocallyFinite.lean, line 48 | For any Ring R, prime p with (p : R) = 0, and Group G with IsPGroup p G and finite subgroup closure of every finite subset, each augmentation-zero element is nilpotent; no uniform exponent or zero power of the whole kernel is asserted. The coefficient and group universes are independent. |
MonoidAlgebra.jacobson_eq_comap_augmentation |
theorem | GroupRings/MonoidAlgebra/Jacobson.lean, line 58 | For any possibly noncommutative or zero Ring R, prime p with (p : R) = 0, and Group G with IsPGroup p G and finite subgroup closure of every finite subset, Ring.jacobson R[G] is the augmentation preimage of Ring.jacobson R; independent coefficient and group universes, with no uniform nilpotence assumption. |
MonoidAlgebra.mem_jacobson_iff_augmentation_mem |
theorem | GroupRings/MonoidAlgebra/Jacobson.lean, line 86 | Under the same locally finite p-group hypotheses, an element lies in the Jacobson radical exactly when its coefficient sum lies in the coefficient radical. |
MonoidAlgebra.single_mem_jacobson_iff |
theorem | GroupRings/MonoidAlgebra/Jacobson.lean, line 97 | Under the same hypotheses, single g r lies in the radical exactly when r does; g=1 gives canonical coefficient inclusion. |
MonoidAlgebra.jacobson_eq_ker_augmentation_of_jacobson_eq_bot |
theorem | GroupRings/MonoidAlgebra/Jacobson.lean, line 107 | Under the same hypotheses and Ring.jacobson R = bottom, the group-algebra Jacobson radical is the canonical augmentation kernel. |
MonoidAlgebra.ker_mapDomainRingHom_mk'_zpowers |
theorem | GroupRings/MonoidAlgebra/Quotient.lean, line 56 | For a normal cyclic subgroup, the quotient index-map kernel is the left ideal generated by the single generator difference, over any ring. |
Ideal.map_pow_le |
theorem | GroupRings/RingTheory/Ideal/Powers.lean, line 40 | Semiring homomorphisms extend left-ideal powers into powers of the extended ideal; equality and target commutativity are not assumed. |
Ideal.pow_mul |
theorem | GroupRings/RingTheory/Ideal/Powers.lean, line 54 | Iteration of left-ideal powers multiplies degrees over any semiring, including zero degrees, without two-sidedness. |
Ideal.pow_eq_bot_iff_forall_list_prod_eq_zero |
theorem | GroupRings/RingTheory/Ideal/Powers.lean, line 32 | The n-th power vanishes exactly when every ordered length-n mixed product vanishes, including n=0. |
MonoidAlgebra.forall_pow_eq_one_of_augmentation_pow_eq_bot |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence.lean, line 45 | Over a nontrivial ring with prime p=0, a zero n-th augmentation power forces every p^k at least n to be a common group exponent. |
MonoidAlgebra.exists_pow_eq_one_of_isNilpotent_augmentation |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence.lean, line 62 | Nilpotence forces one common p-power exponent for an arbitrary group, not only pointwise p-power torsion. |
MonoidAlgebra.exists_pow_eq_one_of_augmentation_products_eq_zero |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence.lean, line 71 | Uniform mixed-product nilpotence has the same common-exponent consequence without a finite-group assumption. |
MonoidAlgebra.isPGroup_of_isNilpotent_augmentation |
theorem | GroupRings/MonoidAlgebra/AugmentationNilpotence.lean, line 82 | The common exponent gives IsPGroup p G as a corollary for nontrivial rings with prime p=0. |
MonoidAlgebra.mem_map_singleOneRingHom_iff |
theorem | GroupRings/MonoidAlgebra/CoefficientIdeals.lean, line 83 | For every left ideal over any semiring and any monoid, extension by constants is equivalent to membership of every coefficient. |
MonoidAlgebra.ker_mapRingHom |
theorem | GroupRings/MonoidAlgebra/CoefficientIdeals.lean, line 126 | The kernel of coefficient change is the extension of the coefficient kernel, without commutativity, nontriviality, additive inverses or surjectivity. |
MonoidAlgebra.quotientCoeffKerEquiv |
def | GroupRings/MonoidAlgebra/CoefficientIdeals.lean, line 155 | For Ring R, Semiring S and surjective f, the coefficient-kernel quotient is S[M], characterized on all classes and every basis coefficient. |
MonoidAlgebra.ker_mapDomainRingHom_comp_mapRingHom |
theorem | GroupRings/MonoidAlgebra/MixedQuotient.lean, line 78 | For Ring R, Semiring S, Group G and Monoid M, the simultaneous kernel is the sum of the subgroup-difference ideal and extended coefficient kernel, with no surjectivity assumptions. |
MonoidAlgebra.quotientMixedKerEquivMrange |
def | GroupRings/MonoidAlgebra/MixedQuotient.lean, line 104 | Surjective coefficients identify the mixed quotient with the monoid algebra of the index range; simultaneous surjectivity also gives the full target. Arbitrary maps instead have the composite range subsemiring as quotient target. |
Polynomial.map_ker_toMultiplicative_toFinsuppIso |
theorem | GroupRings/Polynomial/CoefficientIdeals.lean, line 85 | The stock polynomial equivalence followed by the additive-to-multiplicative index equivalence transports coefficient kernels; companion laws preserve arbitrary coefficient ideals, polynomials and constants. |
MonoidAlgebra.isNoetherianRing_multiplicative_int_iff |
theorem | GroupRings/MonoidAlgebra/CyclicNoetherian.lean, line 45 | For every ring, including noncommutative and zero rings, the infinite cyclic group algebra is left-Noetherian iff its coefficient ring is; uses Laurent ascent from multivariate-polynomials and Mathlib ring transport. |
MonoidAlgebra.isNoetherianRing_iff_of_mulEquiv_int |
theorem | GroupRings/MonoidAlgebra/CyclicNoetherian.lean, line 52 | A supplied group equivalence with Multiplicative Int transports the coefficient criterion, with independent coefficient and group universes and no scalar or carrier replacement. |
MonoidAlgebra.isNoetherianRing_iff_of_finiteIndex_mulEquiv_int |
theorem | GroupRings/MonoidAlgebra/CyclicNoetherian.lean, line 69 | For a finite-index subgroup supplied with an equivalence to the infinite cyclic group, left-Noetherianity of the whole group algebra is equivalent to that of the arbitrary coefficient ring; no normality is needed. |
MonoidAlgebra.isNoetherianRing_multiplicative_int_prod_iff |
theorem | GroupRings/MonoidAlgebra/CyclicNoetherian.lean, line 80 | Products of the infinite cyclic group with any finite group satisfy the same coefficient-ring criterion, using the second projection kernel and its first-coordinate group equivalence. |
MonoidAlgebra.isNoetherianRing_of_fg |
theorem | GroupRings/MonoidAlgebra/Noetherian.lean, line 69 | A finitely generated commutative monoid algebra over an arbitrary left-Noetherian ring is left-Noetherian, in independent universes. The exponent monoid need not be finite and coefficients need not commute. Uses finite-coordinate ascent from multivariate-polynomials and a surjective exponent presentation with coefficient-preserving ring transport. |
MonoidAlgebra.isNoetherianRing_of_injective |
theorem | GroupRings/MonoidAlgebra/Noetherian.lean, line 104 | Over any semiring, an injective group-to-monoid homomorphism descends regular-left Noetherianity of monoid algebras, in three independent universes. |
MonoidAlgebra.isNoetherianRing_subgroup |
theorem | GroupRings/MonoidAlgebra/Noetherian.lean, line 116 | Every subgroup algebra of a left-Noetherian group algebra is left-Noetherian, without finite index or normality. |
MonoidAlgebra.comapDomain_mul_mapDomain |
theorem | GroupRings/MonoidAlgebra/MapDomain.lean, line 41 | Coefficient pullback commutes with right multiplication by a group image in an arbitrary target monoid; coefficients retain their original order. |
MonoidAlgebra.subgroup_fg_of_isNoetherianRing |
theorem | GroupRings/MonoidAlgebra/Noetherian.lean, line 145 | Every subgroup of a group with left-Noetherian group algebra over a nontrivial possibly noncommutative ring is finitely generated; scalar ring is R[G], not R. |
MonoidAlgebra.augmentation_surjective |
theorem | GroupRings/MonoidAlgebra/Augmentation.lean, line 83 | Surjectivity over any semiring and monoid, with independent universes, allowing generic stock Noetherianity transport to the coefficient semiring. |
MonoidAlgebra.ker_mapDomainRingHom_mk' |
theorem | GroupRings/MonoidAlgebra/Quotient.lean, line 47 | For arbitrary ring coefficients, the kernel of the normal-quotient index map is the independently specified left span of the subgroup differences. |
MonoidAlgebra.quotientSpanSubgroupEquiv |
def | GroupRings/MonoidAlgebra/Quotient.lean, line 80 | The first-isomorphism ring equivalence has all-element and full single g r characteristic formulas and is uniquely characterized by its values on quotient classes. |
MonoidAlgebra.existsUnique_comp_mapDomainRingHom_mk'_iff |
theorem | GroupRings/MonoidAlgebra/Quotient.lean, line 144 | An arbitrary unital ring homomorphism into any semiring factors uniquely through the quotient index map exactly when every subgroup basis unit maps to one; the three universes are independent. |
AddMonoidAlgebra.mem_ideal_of_mapDomain_eq_zero |
theorem | GroupRings/MonoidAlgebra/FiberNormalization.lean, line 51 | All-coefficient basis normalization puts mapped-zero elements in a left ideal, over any ring and additive source monoid with an arbitrary target index type. |
AddMonoidAlgebra.ker_mapDomainRingHom_le |
theorem | GroupRings/MonoidAlgebra/FiberNormalization.lean, line 95 | The normalization principle contains an additive-monoid map kernel in the specified left ideal; no surjectivity or section law is required. |
AddMonoidAlgebra.ideal_eq_ker_mapDomainRingHom |
theorem | GroupRings/MonoidAlgebra/FiberNormalization.lean, line 113 | All-coefficient normalization plus the separate ideal-to-kernel containment gives kernel equality. |
AddMonoidAlgebra.mem_ideal_iff_mapDomain_eq_zero |
theorem | GroupRings/MonoidAlgebra/FiberNormalization.lean, line 127 | Membership in a normalized left ideal is equivalent to vanishing under the additive monomial map once the ideal is contained in the kernel. |
MonoidAlgebra.ker_mapDomainRingHom_eq_span_fiber |
theorem | GroupRings/MonoidAlgebra/BinomialKernel.lean, line 58 | For arbitrary monoids and any ring, the induced-map kernel is the ordinary left span of all equal-image unit-basis differences, in independent universes. |
MonoidAlgebra.uniform_fiber_span_of_integer_kernel_fg |
theorem | GroupRings/MonoidAlgebra/UniformBinomialKernel.lean, line 103 | For arbitrary source and target monoids, finite generation of the integer kernel supplies one finite same-fiber pair set generating every ring-coefficient kernel as a left ideal. |
MonoidAlgebra.uniform_fiber_span_of_fg |
theorem | GroupRings/MonoidAlgebra/UniformBinomialKernel.lean, line 122 | An FG commutative source and arbitrary monoid target admit one finite pair set before quantification over every independently universed ring; no coefficient-Noetherian or target-generation assumption. |
MonoidAlgebra.ker_mapDomainRingHom |
theorem | GroupRings/MonoidAlgebra/KernelRange.lean, line 42 | For any group-to-monoid homomorphism and any ring, its algebra pushforward kernel is the independently generated left subgroup relation ideal; no surjectivity, coefficient nontriviality or target group assumption is needed. |
MonoidAlgebra.quotientSpanKerEquivMrange |
def | GroupRings/MonoidAlgebra/KernelRange.lean, line 60 | The canonical quotient is ring-equivalent to the monoid algebra of the stock range submonoid, with all-class and full basis-coefficient formulas and uniqueness. |
MonoidAlgebra.quotientSpanKerEquivOfSurjective |
def | GroupRings/MonoidAlgebra/KernelRange.lean, line 111 | For a surjective group-to-monoid map the range equivalence specializes to the whole target algebra, with characteristic formulas and uniqueness. |
MonoidAlgebra.existsUnique_comp_mapDomainRingHom_mrangeRestrict_iff |
theorem | GroupRings/MonoidAlgebra/KernelRange.lean, line 190 | A homomorphism into any semiring factors uniquely through the range pushforward exactly when every kernel basis unit maps to one; all four universes are independent. |
MonoidAlgebra.existsUnique_comp_mapDomainRingHom_of_surjective_iff |
theorem | GroupRings/MonoidAlgebra/KernelRange.lean, line 157 | Only under index surjectivity is the same unique factorization asserted through the whole target monoid algebra. |
MonoidAlgebra.cosetSum |
def | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 39 | Over any semiring and group, sum coefficients on left cosets into the existing finitely supported coefficient module; cosetSum_single and cosetSum_apply give its basis and finite-support laws. |
MonoidAlgebra.mem_span_subgroup_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 86 | Over any ring, membership in the ordinary left span of subgroup differences iff the coset sum is zero; no normality or nontriviality assumption. |
MonoidAlgebra.single_sub_one_mem_span_subgroup_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 145 | Over a nontrivial ring, a basis difference belongs to the subgroup left ideal iff its index is in the subgroup. |
MonoidAlgebra.span_subgroup_le_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 160 | Over a nontrivial ring, inclusion of subgroup left ideals iff inclusion of subgroups. Forward monotonicity needs no nontriviality and follows from span_mono. |
MonoidAlgebra.span_subgroup_isTwoSided |
theorem | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 118 | Normality implies two-sidedness over any possibly trivial or noncommutative ring. |
MonoidAlgebra.span_subgroup_isTwoSided_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdeals.lean, line 174 | Over a nontrivial ring, two-sidedness of the subgroup left ideal iff the subgroup is normal. |
MonoidAlgebra.span_subgroup_fg_of_fg |
theorem | GroupRings/MonoidAlgebra/SubgroupIdealsFG.lean, line 36 | For any Ring R and Group G in independent universes, H.FG implies FG of the ordinary left ideal spanned by single h 1 - 1; no normality or nontriviality is required. |
MonoidAlgebra.span_subgroup_fg_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdealsFG.lean, line 62 | Over a nontrivial Ring R, the subgroup left ideal is FG iff H is FG, with scalars R[G], not R. |
MonoidAlgebra.ker_augmentation_fg |
theorem | GroupRings/MonoidAlgebra/SubgroupIdealsFG.lean, line 107 | For a Group.FG group over any Ring R, including the zero ring, the augmentation kernel is a finitely generated left ideal. |
MonoidAlgebra.ker_augmentation_fg_iff |
theorem | GroupRings/MonoidAlgebra/SubgroupIdealsFG.lean, line 115 | Over a nontrivial Ring R, the augmentation kernel is FG as a left ideal iff Group.FG G. |
MonoidAlgebra.isUnit_coeff_of_single |
theorem | GroupRings/MonoidAlgebra/Units.lean, line 40 | Under Semiring R and Monoid M, a unit single m r has unit coefficient r, without a nontriviality assumption. |
MonoidAlgebra.isLocalHom_of |
instance | GroupRings/MonoidAlgebra/Units.lean, line 45 | Under Semiring R, Nontrivial R and Monoid M, the basis embedding of R M reflects units. |
MonoidAlgebra.isUnit_single_iff |
theorem | GroupRings/MonoidAlgebra/Units.lean, line 62 | Under Semiring R, Nontrivial R and Monoid M, IsUnit (single m r) iff IsUnit r and IsUnit m. No commutativity, cancellation, group, domain or finiteness hypothesis is required. |
MonoidAlgebra.augmentation |
def | GroupRings/MonoidAlgebra/Augmentation.lean, line 63 | Coefficient-sum ring homomorphism under Semiring R and Monoid M, in independent universes. |
MonoidAlgebra.augmentation_apply |
theorem | GroupRings/MonoidAlgebra/Augmentation.lean, line 68 | The augmentation of x is x.coeff.sum (fun _ r => r). |
MonoidAlgebra.augmentation_single |
theorem | GroupRings/MonoidAlgebra/Augmentation.lean, line 77 | A single basis term augments to its coefficient. |
MonoidAlgebra.ker_augmentation |
theorem | GroupRings/MonoidAlgebra/Augmentation.lean, line 128 | Under Ring R and Monoid M, the kernel is Ideal.span of the range of single m 1 - 1, a left ideal even for noncommutative R. |
Ideal.sub_one_mem_of_mem_submonoid_closure |
theorem | GroupRings/RingTheory/Ideal/MonoidHom.lean, line 31 | For Ring A, Monoid M, a left ideal I and u : M →* A, membership of u s - 1 in I propagates from S to Submonoid.closure S. |
Ideal.sub_one_mem_of_mem_subgroup_closure |
theorem | GroupRings/RingTheory/Ideal/MonoidHom.lean, line 45 | The group-domain companion uses ordinary Subgroup.closure, with no group structure on A or two-sidedness of I. |
MonoidAlgebra.ker_augmentation_eq_span_of_submonoid_closure_eq_top |
theorem | GroupRings/MonoidAlgebra/AugmentationGenerators.lean, line 31 | Under Ring R and Monoid M, Submonoid.closure S = top implies the augmentation kernel is the left span of single s 1 - 1 for s in S. |
MonoidAlgebra.ker_augmentation_eq_span_of_subgroup_closure_eq_top |
theorem | GroupRings/MonoidAlgebra/AugmentationGenerators.lean, line 49 | For Group G, ordinary subgroup generation suffices for the same left-span formula; no normal closure is used. |
Finsupp.kerLsumEquiv |
def | GroupRings/LinearAlgebra/Finsupp/SumKernel.lean, line 56 | For Semiring S, AddCommGroup V, Module S V and b : T, the kernel of lsum ℕ (fun _ => LinearMap.id) is S-linearly equivalent to {t : T // t ≠ b} →₀ V by restriction. The inverse extends and subtracts single b (sum g). |
MonoidAlgebra.sumCoords_basis_apply |
theorem | GroupRings/MonoidAlgebra/AugmentationBasis.lean, line 49 | Under Semiring R and Monoid M, the coordinate sum in the monoid-algebra basis equals augmentation pointwise. |
MonoidAlgebra.ker_augmentation_restrictScalars |
theorem | GroupRings/MonoidAlgebra/AugmentationBasis.lean, line 55 | Under Semiring R and Monoid M, the existing kernel restricted to R is the kernel of the linear coefficient sum composed with coeffLinearEquiv. |
MonoidAlgebra.augmentationKerBasis |
def | GroupRings/MonoidAlgebra/AugmentationBasis.lean, line 72 | Under Ring R and Monoid M, a basis of the augmentation kernel restricted to left coefficient scalars R, indexed by {m : M // m ≠ 1}; vector and repr-coordinate laws are coe_augmentationKerBasis and augmentationKerBasis_repr_apply. No commutativity or nontriviality hypothesis. |
MvLaurentPolynomial |
abbrev | GroupRings/FreeAbelian/LaurentPolynomial.lean, line 26 | Abbreviation for AddMonoidAlgebra A (σ →₀ ℤ), under Semiring A, including noncommutative coefficients. |
AddEquiv.monoidAlgebraMultiplicativeEquivMvLaurentPolynomial |
def | GroupRings/FreeAbelian/LaurentPolynomial.lean, line 35 | Under CommSemiring A and AddCommGroup G, supplied e : G ≃+ (σ →₀ ℤ) induces the A-algebra equivalence; coefficient/group/index universes are independent. |
Quoted from the main results in formalization.yaml of FormalFrontier/group-rings at commit 8e90e656, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.