Commit 2025-01-20 04:58 0f52dbc8

View on Github →

feat: restriction of scalars for root pairings with coefficients in a field (#20384) The headline result is RootPairing.restrictScalars.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/PerfectPairing/Basic.lean

added theorem PerfectPairing.IsPerfectCompl.left_top_iff

added theorem PerfectPairing.IsPerfectCompl.right_top_iff

Created Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

added def RootPairing.restrictScalars'

added theorem RootPairing.restrictScalars_coe_coroot

added theorem RootPairing.restrictScalars_coe_root

added theorem RootPairing.restrictScalars_pairing

added theorem RootPairing.restrictScalars_toPerfectPairing_apply_apply

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.IsCrystallographic.mem_range_algebraMap

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

added theorem RootPairing.ker_corootForm_eq_dualAnnihilator

added theorem RootPairing.ker_rootForm_eq_dualAnnihilator