Commit 2025-04-15 07:29 dabe44e6

View on Github →

chore(*): rename more type vars for *rings (#24022)

Estimated changes

Modified Mathlib/Algebra/LinearRecurrence.lean

modified def LinearRecurrence.IsSolution

modified def LinearRecurrence.charPoly

modified theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init'

modified theorem LinearRecurrence.eq_mk_of_is_sol_of_eq_init

modified theorem LinearRecurrence.geom_sol_iff_root_charPoly

modified theorem LinearRecurrence.is_sol_iff_mem_solSpace

modified theorem LinearRecurrence.is_sol_mkSol

modified def LinearRecurrence.mkSol

modified theorem LinearRecurrence.mkSol_eq_init

modified def LinearRecurrence.solSpace

modified theorem LinearRecurrence.solSpace_rank

modified theorem LinearRecurrence.sol_eq_of_eq_init

modified def LinearRecurrence.toInit

modified def LinearRecurrence.tupleSucc

modified structure LinearRecurrence

Modified Mathlib/Algebra/Ring/InjSurj.lean

modified theorem Function.Injective.leftDistribClass

modified theorem Function.Injective.rightDistribClass

modified theorem Function.Surjective.leftDistribClass

modified theorem Function.Surjective.rightDistribClass

Modified Mathlib/NumberTheory/FLT/Basic.lean

modified theorem FermatLastTheoremWith'.fermatLastTheoremWith

modified def FermatLastTheoremWith'

modified theorem FermatLastTheoremWith.fermatLastTheoremWith'

modified theorem FermatLastTheoremWith.mono

modified def FermatLastTheoremWith

modified theorem fermatLastTheoremWith'_iff_fermatLastTheoremWith

modified theorem fermatLastTheoremWith'_of_semifield