LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical

def UniqueFactorizationMonoid.Mathlib.Meta.Positivity.evalRadical : Mathlib.Meta.Positivity.PositivityExt

Positivity extension for radical. Proves radicals are nonzero.