Reflection

📁 Source: Mathlib/LinearAlgebra/Reflection.lean

Statistics

Metric	Count
Definitions preReflection, reflection	2
Theorems eq_of_preReflection_mapsTo, eq_of_preReflection_mapsTo', bijOn_reflection_of_mapsTo, eq_of_mapsTo_reflection_of_mem, infinite_range_reflection_reflection_iterate_iff, injOn_dualMap_subtype_span_range_range, invOn_reflection_of_mapsTo, involutive_preReflection, involutive_reflection, preReflection_apply, preReflection_apply_self, preReflection_preReflection, reflection_apply, reflection_apply_self, reflection_inv, reflection_mul_reflection_mul_reflection_pow_apply_self, reflection_mul_reflection_mul_reflection_zpow_apply_self, reflection_mul_reflection_pow, reflection_mul_reflection_pow_apply, reflection_mul_reflection_pow_apply_self, reflection_mul_reflection_zpow, reflection_mul_reflection_zpow_apply, reflection_mul_reflection_zpow_apply_self, reflection_reflection_iterate, reflection_symm, mem_invtSubmodule_reflection_iff, mem_invtSubmodule_reflection_of_mem	27
Total	29

Module

Definitions

Name	Category	Theorems
preReflection 📖	CompOp	4 math math: preReflection_apply_self, preReflection_preReflection, preReflection_apply, involutive_preReflection
reflection 📖	CompOp	20 math math: Submodule.mem_invtSubmodule_reflection_of_mem, reflection_inv, reflection_apply_self, reflection_symm, reflection_mul_reflection_pow_apply, invOn_reflection_of_mapsTo, LinearMap.IsReflective.reflective_reflection, LinearMap.IsReflective.isOrthogonal_reflection, reflection_mul_reflection_pow, reflection_reflection_iterate, involutive_reflection, infinite_range_reflection_reflection_iterate_iff, reflection_mul_reflection_pow_apply_self, reflection_mul_reflection_zpow_apply_self, reflection_mul_reflection_zpow_apply, reflection_apply, Submodule.mem_invtSubmodule_reflection_iff, reflection_mul_reflection_mul_reflection_pow_apply_self, reflection_mul_reflection_mul_reflection_zpow_apply_self, reflection_mul_reflection_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijOn_reflection_of_mapsTo 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Set.MapsTo LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection	Set.BijOn	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Set.InvOn.bijOn invOn_reflection_of_mapsTo
eq_of_mapsTo_reflection_of_mem 📖	—	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Set.MapsTo End preReflection Set Set.instMembership	—	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Contrapose.contrapose₁ RingHomInvPair.ids RingHomCompTriple.ids Set.Infinite.mono infinite_range_reflection_reflection_iterate_iff Set.range_subset_iff Function.IsFixedPt.image_iterate Set.BijOn.image_eq Set.BijOn.comp bijOn_reflection_of_mapsTo Set.mem_image_of_mem smul_right_injective instIsTorsionFreeIntOfIsAddTorsionFree Int.instIsCancelMulZero two_ne_zero two_zsmul two_smul
infinite_range_reflection_reflection_iterate_iff 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Set.Infinite Set.range Nat.iterate LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans RingHomCompTriple.ids reflection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomCompTriple.ids reflection_reflection_iterate
injOn_dualMap_subtype_span_range_range 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Function.Embedding Function.instFunLikeEmbedding instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Set.MapsTo End preReflection Set.range	Set.InjOn Submodule SetLike.instMembership Submodule.setLike Submodule.span Submodule.addCommMonoid Submodule.module LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction LinearMap.dualMap Submodule.subtype	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.congr_fun Submodule.subset_span Set.mem_range_self EmbeddingLike.apply_eq_iff_eq Function.instEmbeddingLikeEmbedding eq_of_mapsTo_reflection_of_mem
invOn_reflection_of_mapsTo 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	Set.InvOn LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids involutive_reflection
involutive_preReflection 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	Function.Involutive End preReflection	—	Nat.instAtLeastTwoHAddOfNat preReflection_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass two_smul sub_add_cancel_right smul_neg sub_neg_eq_add sub_add_cancel
involutive_reflection 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	Function.Involutive LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection	—	Nat.instAtLeastTwoHAddOfNat involutive_preReflection
preReflection_apply 📖	mathematical	—	DFunLike.coe End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring preReflection SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Dual NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—
preReflection_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	End preReflection NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat preReflection_apply two_smul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat zero_add Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_neg
preReflection_preReflection 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	preReflection End LinearMap.addCommGroup Ring.toAddCommGroup LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction LinearMap LinearMap.addCommMonoid Dual.eval LinearMap.comp RingHomCompTriple.ids	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext smulCommClass_self RingHomCompTriple.ids preReflection_apply mul_comm smul_sub sub_smul smul_smul sub_mul mul_assoc map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass mul_two add_smul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
reflection_apply 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction	—	Nat.instAtLeastTwoHAddOfNat preReflection_apply
reflection_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reflection NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat preReflection_apply_self
reflection_inv 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	LinearEquiv RingHomInvPair.ids InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearEquiv.automorphismGroup reflection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids
reflection_mul_reflection_mul_reflection_pow_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup reflection Monoid.toNatPow AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Distrib.toAdd Polynomial.eval Polynomial.Chebyshev.S NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Nat.cast_one zpow_natCast reflection_mul_reflection_mul_reflection_zpow_apply_self
reflection_mul_reflection_mul_reflection_zpow_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup reflection DivInvMonoid.toZPow AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Distrib.toAdd Polynomial.eval Polynomial.Chebyshev.S NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids LinearEquiv.mul_apply reflection_mul_reflection_zpow_apply_self map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass reflection_apply Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.neg_congr 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.mul_pf_right Mathlib.Tactic.Ring.sub_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
reflection_mul_reflection_pow 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass reflection LinearMap LinearMap.instAdd LinearMap.id LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Polynomial.eval Polynomial.Chebyshev.S Distrib.toAdd LinearMap.instSub LinearMap.smulRight IsScalarTower.left Ring.toAddCommGroup NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Algebra.id	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomInvPair.ids smulCommClass_self IsScalarTower.left Algebra.to_smulCommClass reflection_mul_reflection_pow_apply
reflection_mul_reflection_pow_apply 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass reflection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Polynomial.eval Polynomial.Chebyshev.S Distrib.toAdd	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids pow_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero zero_sub Polynomial.Chebyshev.S_neg_one Polynomial.eval_zero Polynomial.Chebyshev.S_neg_two Polynomial.eval_neg Polynomial.eval_one zero_add mul_neg mul_one neg_zero zero_smul add_zero EuclideanDomain.zero_div Polynomial.Chebyshev.S_zero Polynomial.Chebyshev.S_sub_two Polynomial.eval_sub Polynomial.eval_mul Polynomial.eval_X Polynomial.eval_add Polynomial.eval_pow Polynomial.Chebyshev.S_sq_add_S_sq pow_succ' LinearEquiv.mul_apply map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass reflection_apply map_smul SemilinearMapClass.toMulActionSemiHomClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Nat.cast_add Nat.cast_one add_assoc add_sub_assoc add_comm Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₃ sub_zero Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass eq_intCast Int.cast_one Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.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.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.Ring.cast_neg Mathlib.Meta.NormNum.isInt_ediv Mathlib.Meta.NormNum.isInt_sub Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
reflection_mul_reflection_pow_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass reflection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Distrib.toAdd Polynomial.eval Polynomial.Chebyshev.S NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Nat.cast_one zpow_natCast reflection_mul_reflection_zpow_apply_self
reflection_mul_reflection_zpow 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv DivInvMonoid.toZPow Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid reflection LinearMap LinearMap.instAdd LinearMap.id LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring Polynomial.eval Polynomial.Chebyshev.S Distrib.toAdd LinearMap.instSub LinearMap.smulRight IsScalarTower.left Ring.toAddCommGroup NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Algebra.id	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomInvPair.ids smulCommClass_self IsScalarTower.left Algebra.to_smulCommClass reflection_mul_reflection_zpow_apply
reflection_mul_reflection_zpow_apply 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DivInvMonoid.toZPow Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid reflection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Polynomial.eval Polynomial.Chebyshev.S Distrib.toAdd	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Nat.cast_one zpow_natCast reflection_mul_reflection_pow_apply mul_comm zpow_neg inv_zpow mul_inv_rev reflection_inv add_right_comm Polynomial.Chebyshev.S_neg_sub_two Polynomial.eval_neg Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.zero_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat
reflection_mul_reflection_zpow_apply_self 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv DivInvMonoid.toZPow Group.toDivInvMonoid LinearEquiv.automorphismGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid reflection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction Distrib.toAdd Polynomial.eval Polynomial.Chebyshev.S NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat Polynomial.Chebyshev.S_sub_two Polynomial.eval_sub Polynomial.eval_mul Polynomial.eval_X Int.induction_on RingHomInvPair.ids zpow_zero Polynomial.Chebyshev.S_zero Polynomial.eval_one zero_sub Polynomial.Chebyshev.S_neg_one Polynomial.eval_zero add_zero one_smul mul_neg MulZeroClass.zero_mul neg_zero zero_smul add_comm zpow_one_add LinearEquiv.mul_apply map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass reflection_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₃ sub_zero Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_one Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.RingNF.mul_neg sub_eq_add_neg zpow_add zpow_neg_one mul_inv_rev reflection_inv Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.LinearCombination.mul_const_eq Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add
reflection_reflection_iterate 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Nat.iterate LinearEquiv RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans RingHomCompTriple.ids reflection AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toSub SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomCompTriple.ids zero_nsmul add_zero smul_smul Nat.cast_smul_eq_nsmul Nat.cast_ofNat Function.iterate_succ' two_smul smul_sub smul_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass reflection_apply_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass reflection_apply neg_sub map_sub map_nsmul map_smul SemilinearMapClass.toMulActionSemiHomClass smul_neg add_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Tactic.Abel.subst_into_smul_upcast Mathlib.Tactic.Abel.term_smulg Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Abel.zero_smulg
reflection_symm 📖	mathematical	DFunLike.coe Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	LinearEquiv.symm RingHomInvPair.ids reflection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids

Module.Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_preReflection_mapsTo 📖	—	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Top.top Submodule Submodule.instTop DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Set.MapsTo Module.End Module.preReflection	—	—	Nat.instAtLeastTwoHAddOfNat map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass RingHomInvPair.ids IsScalarTower.left LinearMap.ext Module.reflection_apply map_sub map_smul SemilinearMapClass.toMulActionSemiHomClass two_smul sub_add_cancel_left smul_neg sub_neg_eq_add sub_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero smulCommClass_self pow_zero CharP.cast_eq_zero CharP.ofCharZero zero_smul RingHomCompTriple.ids sub_self pow_succ' LinearEquiv.coe_toLinearMap_mul add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass add_assoc Nat.cast_succ add_smul one_smul LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo Set.MapsTo.comp isOfFinOrder_iff_pow_eq_one AddLeftCancelSemigroup.toIsLeftCancelAdd LinearMap.instIsTorsionFree IsDomain.toIsCancelMulZero LT.lt.ne'
eq_of_preReflection_mapsTo' 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span DFunLike.coe Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Set.MapsTo Module.End Module.preReflection	LinearMap Submodule.addCommMonoid Submodule.module LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.dualMap Submodule.subtype	—	Nat.instAtLeastTwoHAddOfNat Submodule.subset_span Set.finite_range Set.finite_coe_iff Set.range_inclusion Submodule.span_setOf_mem_eq_top smulCommClass_self eq_of_preReflection_mapsTo Ideal.instIsTorsionFreeSubtypeMemSubmodule

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_invtSubmodule_reflection_iff 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Disjoint Submodule instPartialOrder instOrderBot span Set Set.instSingletonSet	Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids Module.reflection Preorder.toLE PartialOrder.toPreorder LinearMap.ker	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids two_ne_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_sub_cancel_left AddSubgroupClass.toNegMemClass addSubgroupClass sub_mem Module.reflection_apply mem_span_singleton smul_eq_zero IsDomain.toIsCancelMulZero mem_bot Disjoint.eq_bot zero_smul sub_zero
mem_invtSubmodule_reflection_of_mem 📖	mathematical	DFunLike.coe Module.Dual CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Submodule SetLike.instMembership setLike	Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHomInvPair.ids Module.reflection	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids Module.reflection_apply sub_mem_iff_right smul_mem Module.End.mem_invtSubmodule

---

← Back to Index