Equiv.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

43 declarations, 0 contain sorry, 0 declared as axioms

Isomorphisms of restricted products

Restricted products of isomorphic things are isomorphic.

Restricted products of matrices/products/units are isomorphic to matrices/products/units of the restricted product.

Restricted product over a principal filter is isomorphic to a product.

We don't allow topological isomorphisms; they have to go into TopologicalSpace because of imports.

Imports (4)

Imported by 3 files

def Equiv.restrictedProductCongrRight The equivalence between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets line 44 source
Source documentation
The equivalence between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets.

standard axioms: Quot.sound, propext what this means
Statement uses: Set, Filter, Equiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: Equiv.mk, RestrictedProduct.map, Equiv.symm
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def Equiv.restrictedProductCongrRight (φ : (i : ι) → R₁ i ≃ R₂ i)
    (hφ : ∀ᶠ i in 𝓕, Set.BijOn (φ i) (A₁ i) (A₂ i)) :
    Πʳ i, [R₁ i, A₁ i]_[𝓕] ≃ Πʳ i, [R₂ i, A₂ i]_[𝓕] where
…
```
def MulEquiv.restrictedProductCongrRight line 62 source
standard axioms: Quot.sound, propext what this means
Statement uses: SetLike, Filter, Monoid, SubmonoidClass, MulEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: Equiv, Equiv.restrictedProductCongrRight, MulEquiv.toEquiv, MulEquiv.mk
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def MulEquiv.restrictedProductUnits The isomorphism between the units of a restricted product of monoids, and the restricted product of the units of the monoids line 70 source
Source documentation
The isomorphism between the units of a restricted product of monoids, and the restricted product of the units of the monoids.

standard axioms: Quot.sound, propext what this means
Statement uses: Filter, Monoid, SetLike, SubmonoidClass, MulEquiv, Units, RestrictedProduct, Subgroup, Submonoid.units, Submonoid.ofClass
Proof uses: MulEquiv.mk, Equiv.mk, Subtype.mk, Filter.Eventually, Membership.mem, Set, Units.mk, Inv.inv
37 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
def MulEquiv.restrictedProductUnits {ι : Type*} {ℱ : Filter ι}
    {M : ι → Type*} [(i : ι) → Monoid (M i)]
    {S : ι → Type*} [∀ i, SetLike (S i) (M i)] [∀ i, SubmonoidClass (S i) (M i)]
    {A : Π i, S i} :
    (Πʳ i, [M i, A i]_[ℱ])ˣ ≃*
      Πʳ i, [(M i)ˣ, (Submonoid.ofClass (A i)).units]_[ℱ] where
…
```
def RingEquiv.restrictedProductCongrRight The ring isomorphism between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets line 97 source
Source documentation
The ring isomorphism between restricted products on the same index, when each factor is equivalent, with compatibility on the restricted subsets.

standard axioms: Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, RingEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrRight, RingEquiv.toAddEquiv, RingEquiv.mk, AddEquiv.toEquiv
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def RingEquiv.restrictedProductCongrRight (φ : (i : ι) → R₁ i ≃+* R₂ i)
    (hφ : ∀ᶠ i in 𝓕, Set.BijOn (φ i) (A₁ i) (A₂ i)) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕]) ≃+* (Πʳ i, [R₂ i, A₂ i]_[𝓕]) where
…
```
def LinearEquiv.restrictedProductCongrRight The LinearEquiv between restricted products built from LinearEquivs on the factors line 115 source
Source documentation
The LinearEquiv between restricted products built from LinearEquivs on the factors.

standard axioms: Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, LinearEquiv, RingHom.id, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrRight, LinearEquiv.toAddEquiv, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
45 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def LinearEquiv.restrictedProductCongrRight (φ : (i : ι) → R₁ i ≃ₗ[T] R₂ i)
    (hφ : ∀ᶠ i in 𝓕, Set.BijOn (φ i) (A₁ i) (A₂ i)) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕]) ≃ₗ[T] (Πʳ i, [R₂ i, A₂ i]_[𝓕]) where
…
```
def Equiv.restrictedProductCongrLeft' The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 140 source
Source documentation
The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.map, RestrictedProduct, Equiv.symm
Proof uses: Equiv.mk, Subtype.mk, Filter.Eventually, Membership.mem, Equiv.piCongrLeft'
12 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def Equiv.restrictedProductCongrLeft' (e : ι₁ ≃ ι₂) (h : 𝓕₂ = 𝓕₁.map e) :
    Πʳ i, [R₁ i, A₁ i]_[𝓕₁] ≃ Πʳ j, [R₁ (e.symm j), A₁ (e.symm j)]_[𝓕₂] where
…
```
theorem Equiv.restrictedProductCongrLeft'_symm_apply_apply line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.map, RestrictedProduct, Equiv.symm, Equiv.restrictedProductCongrLeft'
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Subtype.mk, Filter.Eventually, Membership.mem, Equiv.piCongrLeft', congrFun, Equiv.restrictedProductCongrLeft'_symm_apply, Equiv.piCongrLeft'_symm_apply_apply, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Equiv.restrictedProductCongrLeft The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 166 source
Source documentation
The equivalence between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.comap, RestrictedProduct
Proof uses: Equiv.symm, Equiv.restrictedProductCongrLeft'
7 instances, coercions and auxiliary constants left out.
```
def Equiv.restrictedProductCongrLeft (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e) :
    Πʳ i, [R₂ (e i), A₂ (e i)]_[𝓕₁] ≃ Πʳ j, [R₂ j, A₂ j]_[𝓕₂] :=
…
```
theorem Equiv.restrictedProductCongrLeft_apply_apply line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.comap, RestrictedProduct, Equiv.restrictedProductCongrLeft
Proof uses: Equiv.restrictedProductCongrLeft'_symm_apply_apply, Equiv.symm, Eq.rec, Filter.map, Eq.symm, Filter.map_equiv_symm
7 instances, coercions and auxiliary constants left out.
def AddEquiv.restrictedProductCongrLeft' Documented declaration: restrictedProductCongrLeft' line 189 source
Source documentation
The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, AddMonoid, AddSubmonoidClass, Equiv, Eq, Filter.map, AddEquiv, RestrictedProduct, Equiv.symm
Proof uses: Equiv.restrictedProductCongrLeft', AddEquiv.mk
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def AddEquiv.restrictedProductCongrLeft' (e : ι₁ ≃ ι₂) (h : 𝓕₂ = 𝓕₁.map e) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃+ (Πʳ j, [R₁ (e.symm j), A₁ (e.symm j)]_[𝓕₂]) where
…
```
def AddEquiv.restrictedProductCongrLeft Documented declaration: restrictedProductCongrLeft line 197 source
Source documentation
The additive monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, AddMonoid, AddSubmonoidClass, Equiv, Eq, Filter.comap, AddEquiv, RestrictedProduct
Proof uses: Equiv.restrictedProductCongrLeft, AddEquiv.mk, Equiv.mk, Equiv.toFun, Equiv.invFun
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def AddEquiv.restrictedProductCongrLeft (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e) :
    Πʳ i, [R₂ (e i), A₂ (e i)]_[𝓕₁] ≃+ Πʳ j, [R₂ j, A₂ j]_[𝓕₂] where
…
```
def MulEquiv.restrictedProductCongrLeft' Documented declaration: restrictedProductCongrLeft' line 220 source
Source documentation
The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Monoid, SubmonoidClass, Equiv, Eq, Filter.map, MulEquiv, RestrictedProduct, Equiv.symm
Proof uses: Equiv.restrictedProductCongrLeft', MulEquiv.mk
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def MulEquiv.restrictedProductCongrLeft' (e : ι₁ ≃ ι₂) (h : 𝓕₂ = 𝓕₁.map e) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃* (Πʳ j, [R₁ (e.symm j), A₁ (e.symm j)]_[𝓕₂]) where
…
```
def MulEquiv.restrictedProductCongrLeft Documented declaration: restrictedProductCongrLeft line 228 source
Source documentation
The multiplicative monoid isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Monoid, SubmonoidClass, Equiv, Eq, Filter.comap, MulEquiv, RestrictedProduct
Proof uses: Equiv.restrictedProductCongrLeft, MulEquiv.mk, Equiv.mk, Equiv.toFun, Equiv.invFun
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def MulEquiv.restrictedProductCongrLeft (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e) :
    Πʳ i, [R₂ (e i), A₂ (e i)]_[𝓕₁] ≃* Πʳ j, [R₂ j, A₂ j]_[𝓕₂] where
…
```
def RingEquiv.restrictedProductCongrLeft' The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 248 source
Source documentation
The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, Equiv, Eq, Filter.map, RingEquiv, RestrictedProduct, Equiv.symm
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrLeft', RingEquiv.mk, AddEquiv.toEquiv
42 instances, coercions and auxiliary constants left out.
```
def RingEquiv.restrictedProductCongrLeft' (e : ι₁ ≃ ι₂) (h : 𝓕₂ = 𝓕₁.map e) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃+* (Πʳ j, [R₁ (e.symm j), A₁ (e.symm j)]_[𝓕₂]) where
…
```
def RingEquiv.restrictedProductCongrLeft The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 256 source
Source documentation
The ring isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, Equiv, Eq, Filter.comap, RingEquiv, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrLeft, RingEquiv.mk, AddEquiv.toEquiv
42 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def RingEquiv.restrictedProductCongrLeft (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e) :
    Πʳ i, [R₂ (e i), A₂ (e i)]_[𝓕₁] ≃+* Πʳ j, [R₂ j, A₂ j]_[𝓕₂] where
…
```
def LinearEquiv.restrictedProductCongrLeft' The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 279 source
Source documentation
The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the right-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, Equiv, Eq, Filter.map, LinearEquiv, RingHom.id, RestrictedProduct, Equiv.symm
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrLeft', LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
48 instances, coercions and auxiliary constants left out.
```
def LinearEquiv.restrictedProductCongrLeft' (e : ι₁ ≃ ι₂) (h : 𝓕₂ = 𝓕₁.map e) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃ₗ[T] (Πʳ j, [R₁ (e.symm j), A₁ (e.symm j)]_[𝓕₂]) where
…
```
def LinearEquiv.restrictedProductCongrLeft The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters line 287 source
Source documentation
The linear isomorphism between restricted products on the same factors on different indices, when the indices are equivalent, with compatibility on the restriction filters. Applying the equivalence on the left-hand side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, Equiv, Eq, Filter.comap, LinearEquiv, RingHom.id, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongrLeft, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
48 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def LinearEquiv.restrictedProductCongrLeft (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e) :
    Πʳ i, [R₂ (e i), A₂ (e i)]_[𝓕₁] ≃ₗ[T] Πʳ j, [R₂ j, A₂ j]_[𝓕₂] where
…
```
def Equiv.restrictedProductCongr The equivalence between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors line 309 source
Source documentation
The equivalence between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.comap, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: Equiv.trans, Equiv.restrictedProductCongrRight, Equiv.restrictedProductCongrLeft
6 instances, coercions and auxiliary constants left out.
```
def Equiv.restrictedProductCongr (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e)
    (φ : (i : ι₁) → R₁ i ≃ R₂ (e i))
    (hφ : ∀ᶠ i in 𝓕₁, Set.BijOn (φ i) (A₁ i) (A₂ (e i))) :
    Πʳ i, [R₁ i, A₁ i]_[𝓕₁] ≃ Πʳ j, [R₂ j, A₂ j]_[𝓕₂] :=
…
```
theorem Equiv.restrictedProductCongr_apply_apply line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.comap, Filter.Eventually, Set.BijOn, RestrictedProduct, Equiv.restrictedProductCongr
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.restrictedProductCongrLeft, RestrictedProduct.map, congrFun, Equiv.restrictedProductCongrRight, Equiv.restrictedProductCongrRight_apply, Equiv.restrictedProductCongrLeft_apply_apply, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Equiv.restrictedProductCongr_symm_apply line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, Eq, Filter.comap, Filter.Eventually, Set.BijOn, RestrictedProduct, Equiv.symm, Equiv.restrictedProductCongr
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
def AddEquiv.restrictedProductCongr The additive monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors line 347 source
Source documentation
The additive monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, AddMonoid, AddSubmonoidClass, Equiv, Eq, Filter.comap, AddEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: Equiv.restrictedProductCongr, AddEquiv.toEquiv, AddEquiv.mk
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def AddEquiv.restrictedProductCongr (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e)
    (φ : (i : ι₁) → R₁ i ≃+ R₂ (e i))
    (hφ : ∀ᶠ i in 𝓕₁, Set.BijOn (φ i) (A₁ i) (A₂ (e i))) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃+ (Πʳ j, [R₂ j, A₂ j]_[𝓕₂]) where
…
```
def MulEquiv.restrictedProductCongr Documented declaration: restrictedProductCongr line 364 source
Source documentation
The multiplicative monoid isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Monoid, SubmonoidClass, Equiv, Eq, Filter.comap, MulEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: Equiv.restrictedProductCongr, MulEquiv.toEquiv, MulEquiv.mk
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def MulEquiv.restrictedProductCongr (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e)
    (φ : (i : ι₁) → R₁ i ≃* R₂ (e i))
    (hφ : ∀ᶠ i in 𝓕₁, Set.BijOn (φ i) (A₁ i) (A₂ (e i))) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃* (Πʳ j, [R₂ j, A₂ j]_[𝓕₂]) where
…
```
def RingEquiv.restrictedProductCongr The ring isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors line 382 source
Source documentation
The ring isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, Equiv, Eq, Filter.comap, RingEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongr, RingEquiv.toAddEquiv, RingEquiv.mk, AddEquiv.toEquiv
42 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def RingEquiv.restrictedProductCongr (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e)
    (φ : (i : ι₁) → R₁ i ≃+* R₂ (e i))
    (hφ : ∀ᶠ i in 𝓕₁, Set.BijOn (φ i) (A₁ i) (A₂ (e i))) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃+* (Πʳ j, [R₂ j, A₂ j]_[𝓕₂]) where
…
```
theorem RingEquiv.restrictedProductCongr_apply_apply line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, Equiv, Eq, Filter.comap, RingEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct, RingEquiv.restrictedProductCongr
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.restrictedProductCongrLeft, RestrictedProduct.map, AddEquiv, Set.MapsTo, RingEquiv.toAddEquiv, id, Eq.refl, congrFun, AddEquiv.restrictedProductCongr, Equiv.restrictedProductCongrRight, AddEquiv.restrictedProductCongr_apply, Equiv.restrictedProductCongrRight_apply, Equiv.restrictedProductCongrLeft_apply_apply, eq_self
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem RingEquiv.restrictedProductCongr_symm_apply line 400 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, SubsemiringClass, Equiv, Eq, Filter.comap, RingEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct, RingEquiv.symm, RingEquiv.restrictedProductCongr
Proof uses: rfl
44 instances, coercions and auxiliary constants left out.
def LinearEquiv.restrictedProductCongr The linear isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors line 421 source
Source documentation
The linear isomorphism between restricted products when the indices and factors are equivalent, provided compatibility criteria on the restriction filters and factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, Equiv, Eq, Filter.comap, LinearEquiv, RingHom.id, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: AddEquiv, AddEquiv.restrictedProductCongr, LinearEquiv.toAddEquiv, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def LinearEquiv.restrictedProductCongr (e : ι₁ ≃ ι₂) (h : 𝓕₁ = 𝓕₂.comap e)
    (φ : (i : ι₁) → R₁ i ≃ₗ[T] R₂ (e i))
    (hφ : ∀ᶠ i in 𝓕₁, Set.BijOn (φ i) (A₁ i) (A₂ (e i))) :
    (Πʳ i, [R₁ i, A₁ i]_[𝓕₁]) ≃ₗ[T] (Πʳ j, [R₂ j, A₂ j]_[𝓕₂]) where
…
```
theorem RingEquiv.restrictedProductCongr_bijOn_structureSubring line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Filter, Ring, SubringClass, Equiv, Eq, Filter.comap, RingEquiv, Set.BijOn, RestrictedProduct, RingEquiv.restrictedProductCongr, Filter.Eventually.of_forall, Subring, RestrictedProduct.structureSubring
Proof uses: Set.MapsTo, Set.BijOn.mapsTo, Equiv.symm, RingEquiv.toEquiv, Set.BijOn.symm, Equiv.invOn, And.intro, And, Set.InjOn, Set.SurjOn, Membership.mem, Set, Iff.mpr, RestrictedProduct.mem_structureSubring_iff, Exists, Equiv.surjective, Eq.rec, Eq.symm, Eq.mpr, Eq.refl and 17 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
def Equiv.restrictedProductProd The bijection between a restricted product of binary products, and the binary product of the restricted products line 468 source
Source documentation
The bijection between a restricted product of binary products, and the binary product of the restricted products.

standard axioms: Quot.sound, propext what this means
Statement uses: Filter, Set, Equiv, RestrictedProduct, Prod, SProd.sprod
Proof uses: Equiv.mk, Prod.mk, RestrictedProduct.map, Prod.fst, Prod.snd, Subtype.mk, Filter.Eventually, Membership.mem
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def Equiv.restrictedProductProd :
    Πʳ i, [A i × B i, C i ×ˢ D i]_[ℱ] ≃ (Πʳ i, [A i, C i]_[ℱ]) × (Πʳ i, [B i, D i]_[ℱ]) where
…
```
lemma Equiv.restrictedProductProd_symm_comp_inclusion line 478 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Filter, LE.le, Eq, Prod, RestrictedProduct, SProd.sprod, Function.comp, Equiv, Equiv.symm, Equiv.restrictedProductProd, Prod.map, RestrictedProduct.inclusion
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
def Equiv.restrictedProductPi The bijection between a restricted product of finite products, and a finite product of restricted products line 497 source
Source documentation
The bijection between a restricted product of finite products, and a finite product of restricted products.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Fintype, Set, Equiv, RestrictedProduct, Set.ofPred, Membership.mem
Proof uses: Equiv.mk, RestrictedProduct.map, RestrictedProduct.mk
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
def Equiv.restrictedProductPi :
    Πʳ i, [Π j, A j i, {f | ∀ j, f j ∈ C j i}]_[ℱ] ≃ Π j, Πʳ i, [A j i, C j i]_[ℱ] where
…
```
lemma Equiv.restrictedProductPi_symm_comp_inclusion line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Set, Filter, LE.le, Eq, RestrictedProduct, Set.ofPred, Membership.mem, Function.comp, Equiv, Equiv.symm, Equiv.restrictedProductPi, Pi.map, RestrictedProduct.inclusion
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
def Equiv.restrictedProductMatrix The bijection between a restricted product of m x n matrices, and m x n matrices of restricted products line 512 source
Source documentation
The bijection between a restricted product of m x n matrices, and m x n matrices of restricted products.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Set, Equiv, RestrictedProduct, Matrix, Set.ofPred, Membership.mem, Filter.cofinite
Proof uses: Equiv.trans, Equiv.restrictedProductPi, Equiv.piCongrRight
2 instances, coercions and auxiliary constants left out.
```
def Equiv.restrictedProductMatrix {ι : Type*} {m n : Type*} [Fintype m] [Fintype n]
    {A : ι → Type*}
    {C : (i : ι) → Set (A i)} :
    Πʳ i, [Matrix m n (A i), {f | ∀ a b, f a b ∈ C i}] ≃ Matrix m n (Πʳ i, [A i, C i]) :=
…
```
def RestrictedProduct.flatten The canonical map from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set line 534 source
Source documentation
The canonical map from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set.

standard axioms: Quot.sound, propext what this means
Statement uses: Filter, Set, Filter.Tendsto, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ
Proof uses: RestrictedProduct.mapAlong, Subtype.mk
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def flatten : Πʳ j, [Π (i : f ⁻¹' {j}), G i, Set.pi Set.univ (fun (i : f ⁻¹' {j}) => C i)]_[𝒢] →
    Πʳ i, [G i, C i]_[ℱ] :=
…
```
lemma RestrictedProduct.flatten_apply line 539 source
standard axioms: Quot.sound, propext what this means
Statement uses: Filter, Set, Filter.Tendsto, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Eq, RestrictedProduct.flatten, Subtype.mk, rfl
12 instances, coercions and auxiliary constants left out.
def RestrictedProduct.flattenEquiv The canonical bijection from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set line 547 source
Source documentation
The canonical bijection from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, Equiv, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ
Proof uses: Equiv.mk, RestrictedProduct.flatten, RestrictedProduct.flattenEquiv.match_1, Filter.Eventually, Subtype.mk
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def flattenEquiv :
    Πʳ j, [Π (i : f ⁻¹' {j}), G i, Set.pi Set.univ (fun (i : f ⁻¹' {j}) => C i)]_[𝒢] ≃
    Πʳ i, [G i, C i]_[ℱ] where
…
```
lemma RestrictedProduct.flatten_equiv_apply line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Equiv, RestrictedProduct.flattenEquiv, Subtype.mk, rfl
16 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.flatten_equiv_symm_apply line 566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Equiv, Equiv.symm, RestrictedProduct.flattenEquiv
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
def RestrictedProduct.flattenEquiv' The equivalence given by flatten when both restricted products are over the cofinite filter line 574 source
Source documentation
The equivalence given by flatten when both restricted products are over the cofinite filter.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Filter.Tendsto, Filter.cofinite, Equiv, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ
Proof uses: RestrictedProduct.flattenEquiv
5 instances, coercions and auxiliary constants left out.
```
def flattenEquiv' :
    Πʳ j, [Π (i : f ⁻¹' {j}), G i, Set.pi Set.univ (fun (i : f ⁻¹' {j}) => C i)] ≃
    Πʳ i, [G i, C i] :=
…
```
lemma RestrictedProduct.flatten_equiv'_apply line 580 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Filter.Tendsto, Filter.cofinite, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Eq, Equiv, RestrictedProduct.flattenEquiv', Subtype.mk, rfl
16 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.flatten_equiv'_symm_apply line 585 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Filter.Tendsto, Filter.cofinite, RestrictedProduct, Set.preimage, Singleton.singleton, Eq, Membership.mem, Set.pi, Set.univ, Equiv, Equiv.symm, RestrictedProduct.flattenEquiv'
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
def RestrictedProduct.principalEquivProd The canonical isomorphism between Πʳ i, [R i, A i]_[𝓟 S] and (Π i ∈ S, R i) × (Π i ∉ S, A i) line 609 source
Source documentation
The canonical isomorphism between Πʳ i, [R i, A i]_[𝓟 S] and (Π i ∈ S, R i) × (Π i ∉ S, A i)

standard axioms: Quot.sound, propext what this means
Statement uses: Set, Decidable, Membership.mem, Equiv, RestrictedProduct, Filter.principal, Prod, Compl.compl
Proof uses: Equiv.mk, Prod.mk, Subtype.mk, Filter.Eventually, dite, Prod.fst, Not, Prod.snd
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
def principalEquivProd : Πʳ i, [R i, A i]_[𝓟 S] ≃
    (Π i : S, A i) × (Π i : (Sᶜ : Set ι), R i) where
…
```
def RestrictedProduct.principalMulEquivProd Additive monoid equivalence of principalEquivProd line 629 source
Source documentation
Additive monoid equivalence of principalEquivProd.

standard axioms: Quot.sound, propext what this means
Statement uses: Set, Decidable, Membership.mem, SetLike, Monoid, SubmonoidClass, MulEquiv, RestrictedProduct, Filter.principal, Prod, Subtype, Compl.compl
Proof uses: Equiv, RestrictedProduct.principalEquivProd, MulEquiv.mk
30 instances, coercions and auxiliary constants left out.
```
def principalMulEquivProd [Π i, Monoid (R i)] [∀ i, SubmonoidClass (T i) (R i)] :
    Πʳ i, [R i, A i]_[𝓟 S] ≃* (Π i : S, A i) × (Π i : (Sᶜ : Set ι), R i) where
…
```
def RestrictedProduct.principalLinearEquivProd Module equivalence version of principalEquivProd line 645 source
Source documentation
Module equivalence version of principalEquivProd.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Set, Decidable, Membership.mem, LinearEquiv, RingHom.id, RestrictedProduct, Filter.principal, Prod, Subtype, Compl.compl
Proof uses: AddEquiv, RestrictedProduct.principalAddEquivSum, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, AddEquiv.toEquiv, Equiv.invFun
63 instances, coercions and auxiliary constants left out.
```
noncomputable def principalLinearEquivProd [Π i, AddCommGroup (R i)]
    [∀ i, Module A (R i)] {C : ∀ i, Submodule A (R i)}
    (S : Set ι) [∀ i, Decidable (i ∈ S)] :
    (Πʳ i, [R i, C i]_[𝓟 S]) ≃ₗ[A] ((Π i : S, C i) ×
      (Π i : (Sᶜ : Set ι), R i)) where
…
```