git grep on perfectoid project

perfectoid.txt

lean-perfectoid-spaces/src$ git grep \^class\
Huber_ring/basic.lean:class Huber_ring (A : Type u) extends comm_ring A, topological_space A, topological_ring A :=
Tate_ring.lean:class Tate_ring (R : Type u) [Huber_ring R] : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_monoid (α : Type*) extends comm_monoid α, linear_order α :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_group (α : Type*) extends comm_group α, linear_ordered_comm_monoid α
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_monoid.is_hom (f : α → β) extends is_monoid_hom f : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_comm_group.is_hom (f : α → β) extends is_group_hom f : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class is_convex (S : set α) : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class is_proper_convex (S : set α) extends is_convex S : Prop :=
for_mathlib/linear_ordered_comm_group.lean:class actual_ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
for_mathlib/linear_ordered_comm_group.lean:class linear_ordered_cancel_comm_monoid_with_zero (α : Type*)
for_mathlib/nonarchimedean/is_subgroups_basis.lean:class is_subgroups_basis {A : Type*} [ring A] {ι : Type*} [inhabited ι] (G : ι → set A) : Prop :=
for_mathlib/topological_field.lean:class topological_division_ring extends topological_ring K : Prop :=
for_mathlib/topological_rings.lean:class ring_with_zero_nhd (α : Type u) extends ring α:=
for_mathlib/uniform_space/uniform_field.lean:class completable_top_field : Prop :=
valuation/basic.lean:class valuation.is_valuation [ring R] (v : R → M) : Prop :=

lean-perfectoid-spaces/src$ git grep \^structure\
Huber_pair.lean:structure is_ring_of_integral_elements {R : Type u}
Huber_pair.lean:structure Huber_pair :=
Huber_ring/basic.lean:structure Huber_ring.ring_of_definition
Spa.lean:structure rational_open_data (A : Huber_pair) :=
adic_space.lean:structure PreValuedRingedSpace :=
adic_space.lean:structure presheaf_of_rings.f_map
adic_space.lean:structure presheaf_of_topological_rings.f_map
adic_space.lean:structure hom (X Y : PreValuedRingedSpace.{u}) :=
adic_space.lean:structure CLVRS :=
for_mathlib/equiv.lean:structure le_equiv (α β : Type*) [has_le α] [has_le β] extends α ≃ β :=
for_mathlib/equiv.lean:structure lt_equiv (α β : Type*) [has_lt α] [has_lt β] extends α ≃ β :=
for_mathlib/linear_ordered_comm_group.lean:structure linear_ordered_comm_monoid.equiv extends equiv α β :=
for_mathlib/linear_ordered_comm_group.lean:structure linear_ordered_comm_group.equiv extends equiv α β :=
for_mathlib/linear_ordered_comm_group.lean:structure linear_ordered_cancel_comm_monoid_with_zero.hom (α : Type*)
for_mathlib/sheaves/covering.lean:structure covering (U : opens α) :=
for_mathlib/sheaves/presheaf.lean:structure presheaf (α : Type u) [topological_space α] :=
for_mathlib/sheaves/presheaf.lean:structure morphism (F G : presheaf α) :=
for_mathlib/sheaves/presheaf.lean:structure iso (F G : presheaf α) :=
for_mathlib/sheaves/presheaf_of_rings.lean:structure presheaf_of_rings (α : Type u) [topological_space α]
for_mathlib/sheaves/presheaf_of_rings.lean:structure morphism (F G : presheaf_of_rings α)
for_mathlib/sheaves/presheaf_of_rings.lean:structure iso (F G : presheaf_of_rings α) :=
for_mathlib/sheaves/presheaf_of_topological_rings.lean:structure presheaf_of_topological_rings (α : Type u) [topological_space α]
for_mathlib/sheaves/presheaf_of_topological_rings.lean:structure morphism (F G : presheaf_of_topological_rings α)
for_mathlib/sheaves/presheaf_of_topological_rings.lean:structure iso (F G : presheaf_of_topological_rings α) :=
for_mathlib/sheaves/sheaf.lean:structure sheaf (α : Type u) [T : topological_space α] :=
for_mathlib/sheaves/sheaf_of_rings.lean:structure sheaf_of_rings (α : Type u) [T : topological_space α] :=
for_mathlib/sheaves/sheaf_of_topological_rings.lean:structure sheaf_of_topological_rings (α : Type u) [T : topological_space α] :=
for_mathlib/sheaves/stalk.lean:structure stalk.elem :=
for_mathlib/topological_groups.lean:structure top_group_equiv extends homeomorph G H :=
perfectoid_space.lean:structure perfectoid_ring (R : Type) [Huber_ring R] extends Tate_ring R : Prop :=

lean-perfectoid-spaces/src$ git grep inductive
lean-projects/lean-perfectoid-spaces/src$ ## no occurrence of the word in any form

lean-perfectoid-spaces/src$ git grep "ℕ"
Spa.lean:    ∀ t₁ ∈ r1.T, ∃ t₂ ∈ r2.T, ∃ N : ℕ, r2.s ^ N * t₂ = r2.s ^ N * (t₁ * k),
Spa.lean:lemma rational_basis.is_basis.pow (T : set A) (hT : is_open (↑(ideal.span T) : set A)) (n : ℕ) :
for_mathlib/linear_ordered_comm_group.lean:lemma one_le_pow_of_one_le {n : ℕ} (H : 1 ≤ x) : 1 ≤ x^n :=
for_mathlib/linear_ordered_comm_group.lean:lemma pow_le_one_of_le_one {n : ℕ} (H : x ≤ 1) : x^n ≤ 1 :=
for_mathlib/linear_ordered_comm_group.lean:lemma eq_one_of_pow_eq_one {n : ℕ} (H : x ^ (n+1) = 1) : x = 1 :=
for_mathlib/nonarchimedean/adic_topology.lean:def adic_basis (I : ideal R) : ℕ → set R := (λ n : ℕ, (I^n).carrier)
for_mathlib/nonarchimedean/adic_topology.lean:lemma is_open_pow_ideal (n : ℕ) : @is_open I.adic_ring _ (I^n).carrier :=
for_mathlib/nonarchimedean/adic_topology.lean:@is_subgroups_basis.is_op _ _ ℕ _ (adic_basis I) _ n
for_mathlib/nonarchimedean/adic_topology.lean:  is-J-adic ↔ (∀ n : ℕ, is_open (↑(J^n) : set R)) ∧ (∀ s ∈ nhds (0 : R), ∃ n : ℕ, ↑(J^n) ⊆ s) :=
for_mathlib/nonarchimedean/adic_topology.lean:lemma is_ideal_adic_pow {J : ideal R} (h : is-J-adic) {n : ℕ} (hn : n > 0) :
for_mathlib/rings.lean:lemma pow_le_pow (I : ideal R) {m n : ℕ} (h : m ≤ n) :
for_mathlib/rings.lean:lemma pow_subset_pow (I : ideal R) {n : ℕ} :
for_mathlib/submodule.lean:lemma fg_pow (h : I.fg) (n : ℕ) : (I^n).fg :=
power_bounded.lean:∀ U ∈ (nhds (0 : R)), ∃ N : ℕ, ∀ n : ℕ, n > N → r^n ∈ U
power_bounded.lean:-- def monoid.set_pow {R : Type*} [monoid R] (T : set R) : ℕ → set R
power_bounded.lean:∀ U ∈ (nhds (0 : R)), ∃ n : ℕ, T ^ n ⊆ U
power_bounded.lean:  have H : (∃ (n : ℕ), (J^n).carrier ⊆ V) :=
prime.lean:def Prime := { p : ℕ // nat.prime p}
prime.lean:instance : has_coe Prime ℕ := ⟨subtype.val⟩

lean-perfectoid-spaces/src$ git grep "ℤ"
Huber_ring/localization.lean:  ∃ (K : finset A), (↑L : set A) ⊆ (↑(span ℤ (T * ↑K)) : set A) :=
Huber_ring/localization.lean:  is_open (↑(T • span ℤ (U : set A)) : set A) :=
Huber_ring/localization.lean:  replace hV : span ℤ _ ≤ span ℤ _ := span_mono hV,
Huber_ring/localization.lean:  -- First observe: I^(m+1) = L • I^m as A₀-ideal, but also as ℤ-submodule
Huber_ring/localization.lean:  erw [subtype.coe_mk (↑(T • span ℤ ↑U) : set A), @submodule.smul_def ℤ, span_mul_span],
Huber_ring/localization.lean:      rcases (finsupp.mem_span_iff_total ℤ).mp (by rw set.image_id; exact ha) with ⟨l, hl₁, hl₂⟩,
Huber_ring/localization.lean:      show (↑(_ : ℤ) * _) * _ ∈ _,
for_mathlib/submodule.lean:  (↑(S • I) : set R) = (↑(S • (span ℤ (↑I : set R))) : set R) :=
for_mathlib/submodule.lean:  add_group.closure s = ↑(span ℤ s) :=
for_mathlib/submodule.lean:  (↑(span ℤ s) : set R) = s :=
for_mathlib/submodule.lean:lemma span_span_int (S' : set B) [is_subring S'] (X : set B) : span S' ↑(span ℤ X) = span S' X :=
power_bounded.lean:    (↑((V : set R) • span ℤ B) : set R) ⊆ U :=
buzzard@ebony:~/lean-projects/lean-perfectoid-spaces/src$