Theorems · Theorem · nonassociative algebras

RootPairing.mk.congr_simp

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (toLinearMap toLinearMap_1 : M →ₗ[R] N →ₗ[R] R)
  (e_toLinearMap : toLinearMap = toLinearMap_1) [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] (root root_1 : ι ↪ M)
  (e_root : root = root_1) (coroot coroot_1 : ι ↪ N) (e_coroot : coroot = coroot_1)
  (root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) (reflectionPerm reflectionPerm_1 : ι → ι ≃ ι)
  (e_reflectionPerm : reflectionPerm = reflectionPerm_1)
  (reflectionPerm_root : ∀ (i j : ι), root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j))
  (reflectionPerm_coroot :
    ∀ (i j : ι), coroot j - (toLinearMap (root i)) (coroot j) • coroot i = coroot ((reflectionPerm i) j)),
  { toLinearMap := toLinearMap, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
      root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm, reflectionPerm_root := reflectionPerm_root,
      reflectionPerm_coroot := reflectionPerm_coroot } =
    { toLinearMap := toLinearMap_1, isPerfPair_toLinearMap := ⋯, root := root_1, coroot := coroot_1,
      root_coroot_two := ⋯, reflectionPerm := reflectionPerm_1, reflectionPerm_root := ⋯, reflectionPerm_coroot := ⋯ }

Defined in

Mathlib.LinearAlgebra.RootSystem.Defs

Cited by

1 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleLinearMap.IsPerfPair