Congruence of series is symmetric.
ProvedTypeDensity.SCongr.symmtype-density
Congruence of series is symmetric.
Preamble
import Definitions.Def_TypeDensity_Basic import Definitions.Def_TypeDensity_Reciprocity_Defs import Definitions.Def_TypeDensity_Reciprocity_Quantum import Mathlib.FieldTheory.RatFunc.Basic import Mathlib.MeasureTheory.Measure.Haar.Unique import Mathlib.NumberTheory.ArithmeticFunction.Moebius import Mathlib.NumberTheory.Padics.PadicIntegers import Mathlib.RingTheory.IntegralClosure.IntegralRestrict import Mathlib.RingTheory.MvPowerSeries.Basic import Mathlib.RingTheory.RamificationInertia.Basic import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology import Mathlib.FieldTheory.RatFunc.AsPolynomial import Mathlib.RingTheory.PowerSeries.Expand import Mathlib.RingTheory.PowerSeries.Log set_option autoImplicit false open TypeDensity
Formal statement
theorem TypeDensity.SCongr.symm {n : ℕ} {f g : Ser} (h : SCongr n f g) : SCongr n g f := by sorrySource
TypeDensity/Reciprocity/Quantum.lean#L846-L848