test module

`Tests.GradientAlgebra`

0 named declarations scanned from Tests/GradientAlgebra.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/GradientAlgebra.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra

-- Focused API smoke checks for the reusable Chapter 8 gradient rules.
-- Refresh against the canonical Chapter 1 source-index evidence entry point.
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.HasGradientAt.mul
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.HasGradientAt.comp_real
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.HasGradientAt.inv
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.HasGradientAt.div
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.gradient_mul_eq_of_differentiableAt
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.gradient_comp_real_eq_of_differentiableAt
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.gradient_inv_eq_of_differentiableAt
#check AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebra.gradient_div_eq_of_differentiableAt