feat: added lambda rings

[Cobord]

Description:

This does lambda rings. It is mostly over rationals so we can concern ourselves only with the psi^n operations and not the more complicated lambda^n operations. Doing the more general case could be another PR. This also includes the Getzler type formulation as the map involving Lambda_R the ring of symmetric functions in countably many variables (which again because R is assumed as [Algebra Q R] is described with it's power sum generators). That is to say the Plethystic action. Homomorphisms of such lambda rings are also covered. In particular, those of inclusions of subrings closed under those psi^n operations. In addition, one of the primary motivating examples of K(GL(n)/P) otimes_Z Q is described as such an instance to provide an example that is not Lambda_R.

This was done with Claude Code for generating initial versions but I had not given a good full prompt about prefering psi^n over lambda^n or using a structure instead of a prop in AdamsHom so I ended up rewriting most of those parts by hand anyway. The exception is the PrimeExtend file which is about only giving the psi^p instead of all of the psi^n, but abstracted away from those particular details per clarifying instructions after an initial version.

Because PrimeExtend is so much, this has a tag of

LLM-generated

In addition even though it is in RingTheory it is highly relevant to
t-combinatorics
in the sense of algebraic combinatorics due to use of ring of symmetric functions in countably many variables.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 6696290153

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.LambdaRing.PrimeExtend (new file)	820
Mathlib.RingTheory.LambdaRing.SymmetricFunctions (new file)	1192
Mathlib.RingTheory.LambdaRing.AdamsOperations (new file)	1219
Mathlib.RingTheory.LambdaRing.AdamsHom (new file)	1220
Mathlib.RingTheory.LambdaRing.KFlagExample (new file)	1221

---

Declarations diff (regex)

+ AdamsHom
+ AdamsHom.ofRestrict
+ AdamsOperations
+ AdamsOperations.ofPrimes
+ AdamsOperations.restrict
+ KFlag
+ KFlag.L
+ LeviPerm
+ ParabSubalgebra
+ ParabSubalgebraAux
+ SymmFun
+ SymmFun.actAdamsHom
+ act
+ act_add
+ act_apply_X
+ act_comp
+ act_eq_comp
+ act_mul_p
+ act_p
+ act_p_one
+ act_psi
+ antipode
+ antipode_X
+ antipode_p
+ comp_apply
+ comp_apply_X
+ comp_assoc
+ comp_p_one_left
+ comp_p_one_right
+ comp_psi
+ comul
+ comul_X
+ comul_apply_X
+ comul_p
+ counit
+ counit_X
+ counit_apply_X
+ counit_p
+ ext
+ extendPrimes
+ extendPrimes_mul
+ extendPrimes_one
+ extendPrimes_prime
+ extendPrimes_prime_mul
+ extendPrimes_prime_mul_mem
+ extendPrimes_prime_mul_notMem
+ flagPsi
+ flagPsiAux
+ flagPsiAux_apply_X
+ flagPsiAux_mul
+ flagPsiAux_one
+ flagPsiAux_rename_comm
+ flagPsi_mul
+ flagPsi_one
+ id
+ instance : AdamsOperations R (SymmFun R)
+ instance : AdamsOperations ℚ (KFlag n)
+ instance : Algebra ℚ (KFlag n)
+ instance : Bialgebra R (SymmFun R)
+ instance : CommRing (KFlag n)
+ instance : FunLike (AdamsHom R A B) A B
+ instance : HopfAlgebra R (SymmFun R)
+ isUnit_natCast_of_algebra_rat
+ mem_ParabSubalgebraAux
+ p
+ p_def
+ parabAdamsOperations
+ parabSubalgebraAux_psi_mem
+ parabSubalgebra_psi_mem
+ pc
+ psi
+ psi_apply_X
+ psi_mul
+ psi_one
+ psi_p
+ realize
+ realize_p
+ subtype_erase_insert_of_prime
+ subtype_insert_of_prime
+ support_single_add
+ toAlgHom_apply
++ comp

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Increase in strong tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (strong)
501	2	erw
6985	2	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 6696290153
Reference commit a6180e1994

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Cobord]

t-combinatorics

[Cobord]

LLM-generated