Commit 2025-05-19 10:23 8e985cdb
View on Github →chore(Algebra/Order/Nonneg/Basic): remove duplicate Nonneg.pow_nonneg (#24997)
This lemma already exists in the root namespace, so it is a duplicate.
chore(Algebra/Order/Nonneg/Basic): remove duplicate Nonneg.pow_nonneg (#24997)
This lemma already exists in the root namespace, so it is a duplicate.