Documentation
Qq
Search
Google site search
return to top
source
Imports
Init
Qq.AssertInstancesCommute
Qq.Delab
Qq.Macro
Qq.Match
Qq.MetaM
Imported by
Mathlib.Tactic.Positivity.Basic
Mathlib.Tactic.Bound.Attribute
Mathlib.Data.Finset.Attr
Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Tactic.FunProp.FunctionData
Mathlib.Tactic.Positivity.Core
Mathlib.Util.SynthesizeUsing
Mathlib.Tactic.Common
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.TFAE
Mathlib.Util.Qq
Mathlib.Tactic.Tauto