OfBilinear

📁 Source: Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Statistics

Metric	Count
Definitions IsReflective, coroot, ofBilinear	3
Theorems apply_self_mul_coroot_apply, coroot_apply_self, dvd_two_mul, isOrthogonal_reflection, of_dvd_two, reflective_reflection, regular, smul_coroot	8
Total	11

LinearMap

Definitions

Name	Category	Theorems
IsReflective 📖	CompData	1 math math: IsReflective.of_dvd_two

LinearMap.IsReflective

Definitions

Name	Category	Theorems
coroot 📖	CompOp	5 math math: smul_coroot, apply_self_mul_coroot_apply, reflective_reflection, isOrthogonal_reflection, coroot_apply_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_self_mul_coroot_apply 📖	mathematical	LinearMap.IsReflective	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id coroot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Algebra.to_smulCommClass Nat.instAtLeastTwoHAddOfNat dvd_two_mul
coroot_apply_self 📖	mathematical	LinearMap.IsReflective	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike coroot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Algebra.to_smulCommClass IsRegular.left regular Nat.instAtLeastTwoHAddOfNat apply_self_mul_coroot_apply mul_comm
dvd_two_mul 📖	mathematical	LinearMap.IsReflective	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Algebra.to_smulCommClass
isOrthogonal_reflection 📖	mathematical	LinearMap.IsReflective LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	LinearMap.IsOrthogonal DFunLike.coe LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.reflection coroot coroot_apply_self	—	Algebra.to_smulCommClass RingHomInvPair.ids coroot_apply_self Module.reflection_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass IsRegular.left regular Nat.instAtLeastTwoHAddOfNat mul_sub apply_self_mul_coroot_apply sub_eq_iff_eq_add LinearMap.IsSymm.eq RingHom.id_apply mul_assoc mul_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add
of_dvd_two 📖	mathematical	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	LinearMap.IsReflective	—	Algebra.to_smulCommClass Nat.instAtLeastTwoHAddOfNat IsRegular.of_ne_zero two_ne_zero Dvd.dvd.mul_right
reflective_reflection 📖	mathematical	LinearMap.IsSymm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap.IsReflective	DFunLike.coe LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.reflection coroot coroot_apply_self	—	Algebra.to_smulCommClass RingHomInvPair.ids coroot_apply_self isOrthogonal_reflection regular LinearEquiv.eq_symm_apply Nat.instAtLeastTwoHAddOfNat dvd_two_mul
regular 📖	mathematical	LinearMap.IsReflective	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
smul_coroot 📖	mathematical	LinearMap.IsReflective	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Algebra.id DFunLike.coe LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module coroot AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing	—	Algebra.to_smulCommClass LinearMap.ext Nat.instAtLeastTwoHAddOfNat apply_self_mul_coroot_apply nsmul_eq_mul

RootPairing

Definitions

Name	Category	Theorems
ofBilinear 📖	CompOp	—

---

← Back to Index