+ instance : Algebra A K := inferInstanceAs <| Algebra A.toSubring K
+ instance : CommRing A := inferInstanceAs <| CommRing A.toSubring
+ instance : IsDomain A := inferInstanceAs <| IsDomain A.toSubring
+ instance : Module (MonoidAlgebra k G) ρ.asModule
+ instance : Module (ResidueField R) (CotangentSpace R)
- Arrow.inhabited
- Cotangent.isScalarTower
- Cotangent.moduleOfTower
- KaehlerDifferential.module
- NatOrdinal.instLinearOrder
- NatOrdinal.instNoMaxOrder
- NatOrdinal.instOrderBot
- NatOrdinal.instSuccOrder
- NatOrdinal.instZeroLEOneClass
- NatOrdinal.uncountable
- ResidueFieldCommRing
- ResidueFieldInhabited
- SheafCat
- algebra
- algebra'
- commRing
- commutator_characteristic
- cotangentModule
- inhabited
- instAlgebra
- instContinuousLinearMapClass
- instContinuousMapClass
- instFintype
- instFunLike
- instGroup
- instModuleAsModule
- instMonoidHomClass
- instRing
- instance (C) [Quiver C] : Inhabited (HomRel C)
- instance (X : C) : Preorder (J.Cover X)
- instance (α : Type*) : Inhabited (SetSemiring α)
- instance (α : Type*) : OrderBot (SetSemiring α)
- instance (α : Type*) : PartialOrder (SetSemiring α)
- instance : AddCommGroup (KaehlerDifferential R S) := inferInstanceAs <|
- instance : AddCommGroup (TangentSpace I x) := inferInstanceAs (AddCommGroup E)
- instance : AddCommGroup I.Cotangent := by delta Cotangent; infer_instance
- instance : AddCommMonoid (ρ.asModule) := inferInstanceAs <| AddCommMonoid V
- instance : AlgEquivClass p.Gal F p.SplittingField p.SplittingField
- instance : Algebra (ZMod p) (GaloisField p n) := SplittingField.algebra _
- instance : Algebra A K
- instance : CanonicallyOrderedAdd PrimeMultiset
- instance : CanonicallyOrderedAdd ℕ∞ := WithTop.canonicallyOrderedAdd
- instance : Category (Arrow T) := commaCategory
- instance : Category (OpensLeCover U) := ObjectProperty.FullSubcategory.category _
- instance : Category (Skeleton C) := by
- instance : CharP (GaloisField p n) p
- instance : CharZero ℕ∞ := inferInstanceAs (CharZero (WithTop ℕ))
- instance : CommGroup (PontryaginDual A)
- instance : CommRing A
- instance : CompleteLinearOrder ENat
- instance : ContinuousConstSMul 𝕜 (TangentSpace I x) := inferInstanceAs (ContinuousConstSMul 𝕜 E)
- instance : ContinuousSMul 𝕜 (TangentSpace I x) := inferInstanceAs (ContinuousSMul 𝕜 E)
- instance : CountableInterFilter (countableGenerate g) := by
- instance : Epi (toTotalQuotientPresheaf F) := epi_toLocalizationPresheaf _
- instance : EquivLike p.Gal p.SplittingField p.SplittingField
- instance : Field (GaloisField p n)
- instance : Finite (GaloisField p n)
- instance : FiniteDimensional (ZMod p) (GaloisField p n) := by
- instance : FunLike (PontryaginDual A) A Circle
- instance : Inhabited (@GaloisField 2 (Fact.mk Nat.prime_two) 1) := ⟨37⟩
- instance : Inhabited (Monoid.CoprodI M)
- instance : Inhabited (PontryaginDual A)
- instance : Inhabited (SingleObj α)
- instance : Inhabited (TensorAlgebra R M) := RingQuot.instInhabited _
- instance : Inhabited I.Cotangent := ⟨0⟩
- instance : Injective <| syzygies f := injective_under (cokernel f)
- instance : IsDomain A
- instance : IsOrderedCancelAddMonoid PrimeMultiset
- instance : IsOrderedRing ℕ∞ := WithTop.instIsOrderedRing
- instance : IsScalarTower S (S ⊗[R] S) Ω[S⁄R]
- instance : IsSplittingField (ZMod p) (GaloisField p n) (X ^ p ^ n - X)
- instance : IsTopologicalAddGroup (TangentSpace I x) := inferInstanceAs (IsTopologicalAddGroup E)
- instance : IsTopologicalGroup (PontryaginDual A)
- instance : LinearOrderedCommGroupWithZero (ValueGroup A) := by
- instance : Module (ResidueField R) (CotangentSpace R) := Ideal.cotangentModule _
- instance : Module k ρ.asModule := inferInstanceAs <| Module k V
- instance : Module 𝕜 (TangentSpace I x) := inferInstanceAs (Module 𝕜 E)
- instance : Monoid (Monoid.CoprodI M) := by
- instance : Nonempty Ω[S⁄R] := ⟨0⟩
- instance : OrderBot PrimeMultiset
- instance : OrderBot ℕ∞ := WithTop.orderBot
- instance : OrderTop ℕ∞ := WithTop.orderTop
- instance : OrderedSub PrimeMultiset
- instance : OrderedSub ℕ∞ := inferInstanceAs (OrderedSub (WithTop ℕ))
- instance : PathConnectedSpace (TangentSpace I x) := inferInstanceAs (PathConnectedSpace E)
- instance : Semiring (TensorAlgebra R M) := RingQuot.instSemiring _
- instance : Subgroup.Normal (commutator G) := Subgroup.commutator_normal ⊤ ⊤
- instance : SuccOrder ℕ∞ := inferInstanceAs (SuccOrder (WithTop ℕ))
- instance : T2Space (PontryaginDual A)
- instance : TopologicalSpace (PontryaginDual A)
- instance : TopologicalSpace (TangentSpace I x) := inferInstanceAs (TopologicalSpace E)
- instance : WellFoundedLT ℕ∞ := inferInstanceAs (WellFoundedLT (WithTop ℕ))
- instance [DiscreteTopology A] : CompactSpace (PontryaginDual A)
- instance [Inhabited C] : Inhabited (Skeleton C)
- instance [IsNoetherian R I] : IsNoetherian R I.Cotangent
- instance {S : Type*} [DistribSMul S K] [IsScalarTower S K K] : SMul S (SplittingField f)
- instance {m : ℤ} : AddCommGroup (StandardOneDimIsocrystal p k m)
- instance {m : ℤ} : Module K(p, k) (StandardOneDimIsocrystal p k m)
- instance {α : Type*} : Unique (SingleObj α)
- instance {α} [CoeSort C α] : CoeSort (Skeleton C) α
- isScalarTower
-- instContinuousAdd
-- instInhabited
-- instTopologicalSpace
--- instAddCommMonoid
--- instModule

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).