'ConnesRigidity.exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'ConnesRigidity.exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
exists_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors : ∃ Γ Λ,
  Group.FG Γ.Carrier ∧
    Group.FG Λ.Carrier ∧
      IsICC Γ ∧
        HasKazhdanPropertyT Γ ∧
          IsICC Λ ∧ HasKazhdanPropertyT Λ ∧ TracialGroupFactorsIsomorphic Γ Λ ∧ ¬GroupsIsomorphic Γ Λ
exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors : ∃ Λ Γ,
  Group.FG Λ.Carrier ∧
    (∀ (n : ℕ), Group.FG (Γ n).Carrier) ∧
      IsICC Λ ∧
        (∀ (n : ℕ), IsICC (Γ n)) ∧
          HasKazhdanPropertyT Λ ∧
            (∀ (n : ℕ), HasKazhdanPropertyT (Γ n)) ∧
              (∀ (n : ℕ), TracialGroupFactorsIsomorphic (Γ n) Λ) ∧
                (∀ (m n : ℕ), TracialGroupFactorsIsomorphic (Γ m) (Γ n)) ∧
                  (∀ ⦃m n : ℕ⦄, m ≠ n → ¬GroupsIsomorphic (Γ m) (Γ n)) ∧ ∀ (n : ℕ), ¬GroupsIsomorphic Λ (Γ n)
'ConnesRigidity.paper_factors_isomorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.lambda_isICC' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.gamma_isICC' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.lambda_hasKazhdanPropertyT_unconditional' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.gamma_hasKazhdanPropertyT_unconditional' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.paperAnalyticInput' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.suslinRelativeElementaryGeneration' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.actingGroup_hasKazhdanPropertyT' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.semidirect_isICC' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.k_D_orbit_infinite' depends on axioms: [propext, Classical.choice, Quot.sound]
'ConnesRigidity.kEAddAction_orbit_infinite_of_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
lambdaGroup : CountableDiscreteGroup
gammaGroup : ℕ → CountableDiscreteGroup
Lambda : Type
Gamma : ℕ → Type
