Theorems · Theorem · ring theory

isSelfAdjoint_smul_of_mem_skewAdjoint

∀ {R : Type u_1} {A : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup A] [inst_2 : Module R A]
  [inst_3 : StarAddMonoid R] [inst_4 : StarAddMonoid A] [StarModule R A] {r : R},
  r ∈ skewAdjoint R → ∀ {a : A}, a ∈ skewAdjoint A → IsSelfAdjoint (r • a)

Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.

Defined in: Mathlib.Algebra.Star.SelfAdjoint
Cited by: 1 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Quot.sound
Assumes: Ring AddCommGroup Module StarAddMonoid StarAddMonoid StarModule

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
Ringstatement and proof · cited by 7,463
AddSubgroupstatement · cited by 3,232
StarModulestatement and proof · cited by 570
IsSelfAdjointstatement · cited by 545
StarAddMonoidstatement and proof · cited by 296
skewAdjointstatement and proof · cited by 34
StarModule.star_smulproof · cited by 34
neg_smul_negproof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

IsSelfAdjoint.I_smul_of_mem_skewAdjointproof · cited by 0