Algebraize

📁 Source: Mathlib/Tactic/Algebraize.lean

Statistics

Metric	Count
Definitions algebraizeAttr, algebraizeGetParam, Config, properties, addAlgebraInstanceFromRingHom, addIsScalarTowerInstanceFromRingHomComp, addProperties, elabAlgebraizeConfig, instInhabitedConfig, default, algebraizeTermSeq, tacticAlgebraize__, tacticAlgebraize_only__	13
Theorems	0
Total	13

Lean.Attr

Definitions

Name	Category	Theorems
algebraizeAttr 📖	CompOp	—
algebraizeGetParam 📖	CompOp	—

Mathlib.Tactic

Definitions

Name	Category	Theorems
algebraizeTermSeq 📖	CompOp	—
tacticAlgebraize__ 📖	CompOp	—
tacticAlgebraize_only__ 📖	CompOp	—

Mathlib.Tactic.Algebraize

Definitions

Name	Category	Theorems
Config 📖	CompData	—
addAlgebraInstanceFromRingHom 📖	CompOp	—
addIsScalarTowerInstanceFromRingHomComp 📖	CompOp	—
addProperties 📖	CompOp	—
elabAlgebraizeConfig 📖	CompOp	—
instInhabitedConfig 📖	CompOp	—

Mathlib.Tactic.Algebraize.Config

Definitions

Name	Category	Theorems
properties 📖	CompOp	—

Mathlib.Tactic.Algebraize.instInhabitedConfig

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index